isClosed_iSup_iff — Mathlib

English

For a family t : ι → TopologicalSpace α and a subset s ⊆ α, s is closed in ⨆ i t i iff s is closed in every t i.

Русский

Для семейства t : ι → TopologicalSpace α и множества s ⊆ α, s замкнуто в ⨆ i t i тогда и только тогда, когда s замкнуто во всех t i.

LaTeX

$$$\\mathrm{IsClosed}[\\bigvee_i t_i]\,s \\iff \\forall i, \\mathrm{IsClosed}[t_i]\,s$$$

Lean4

theorem isClosed_iSup_iff {s : Set α} : IsClosed[⨆ i, t i] s ↔ ∀ i, IsClosed[t i] s := by
  simp only [← @isOpen_compl_iff _ _ (⨆ i, t i), ← @isOpen_compl_iff _ _ (t _), isOpen_iSup_iff]

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