iInter — Mathlib

English

Let ι be a finite index set and f(i) ⊆ X for each i. If every f(i) is retrocompact in X, then the intersection over all i of f(i) is retrocompact.

Русский

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

LaTeX

$$[Finite ι] (∀ i, IsRetrocompact (f(i))) → IsRetrocompact (⋂ i, f(i))$$

Lean4

theorem iInter [Finite ι] {f : ι → Set X} (hf : ∀ i, IsRetrocompact (f i)) : IsRetrocompact (⋂ i, f i) :=
  infClosed_isRetrocompact.iInf_mem .univ hf

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