finsetSup — Mathlib

English

If t is a finite set and each t(i) is retrocompact, then the FinsetSup (finite union) is retrocompact.

Русский

Если t — конечное множество индексов и каждый t(i) ретрокомпактен, то FinsetSup (конечное объединение) ретрокомпактно.

LaTeX

$$$\forall i, i \in s \Rightarrow \text{IsRetrocompact}(t(i)) \Rightarrow \text{IsRetrocompact}(\,s.\mathrm{sup} t\,)$$$

Lean4

theorem finsetSup {ι : Type*} {s : Finset ι} {t : ι → Set X} (ht : ∀ i ∈ s, IsRetrocompact (t i)) :
    IsRetrocompact (s.sup t) := by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.sup_cons]
    exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht

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