biInter — Mathlib

English

Let ι be a finite index set and t ⊆ ι finite. If each f(i) with i ∈ t is retrocompact, then the intersection over i ∈ t of f(i) is retrocompact.

Русский

Пусть ι — конечный индексный набор и t ⊆ ι конечен. Если каждый f(i) с i ∈ t ретрокомпактен, то пересечение по i ∈ t f(i) ретрокомпактно.

LaTeX

$$IsRetrocompact (⋂ i ∈ t, f i)$$

Lean4

theorem biInter {ι : Type*} {f : ι → Set X} {t : Set ι} (ht : t.Finite) (hf : ∀ i ∈ t, IsRetrocompact (f i)) :
    IsRetrocompact (⋂ i ∈ t, f i) :=
  infClosed_isRetrocompact.biInf_mem ht .univ hf

Похожие утверждения