finsetInf' — Mathlib

English

Let s be a nonempty finite set of indices and t(i) a family of subsets of X such that each t(i) is retrocompact. Then the inf' intersection s.inf' hs t is retrocompact.

Русский

Пусть s — непустое конечное множество индексов и t(i) — семейство подмножеств X, для каждого i ∈ s множество t(i) ретрокомпактно. Тогда пересечение s.inf' hs t ретрокомпактно.

LaTeX

$$$(\\forall i \\in s, IsRetrocompact(t(i))) \\rightarrow IsRetrocompact\\left(s.inf' hs\\ t\\right)$$

Lean4

theorem finsetInf' {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X} (ht : ∀ i ∈ s, IsRetrocompact (t i)) :
    IsRetrocompact (s.inf' hs t) := by rw [Finset.inf'_eq_inf]; exact .finsetInf ht

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