isClosed_iff_iSup — Mathlib

English

IsClosed s is equivalent to that every iSup of a family of elements in s lies in s.

Русский

Замкнутость множества эквивалентна тому, что любой iSup семейства элементов в s принадлежит s.

LaTeX

$$IsClosed s ↔ ∀ {ι}, Nonempty ι → ∀ f : ι → Ordinal, (∀ i, f i ∈ s) → (iSup f) ∈ s$$

Lean4

theorem isClosed_iff_iSup :
    IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ f : ι → Ordinal, (∀ i, f i ∈ s) → ⨆ i, f i ∈ s :=
  by
  use fun hs ι hι f hf => (mem_iff_iSup_of_isClosed hs).2 ⟨ι, hι, f, hf, rfl⟩
  rw [← closure_subset_iff_isClosed]
  intro h x hx
  rcases mem_closure_iff_iSup.1 hx with ⟨ι, hι, f, hf, rfl⟩
  exact h hι f hf

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