mem_iff_iSup_of_isClosed — Mathlib

English

If s is closed, then a ∈ s is equivalent to an existential iSup representation with a family in s.

Русский

Если s замкнуто, то a ∈ s эквивалентно существованию iSup-представления через семейство элементов s.

LaTeX

$$IsClosed s ⇒ (a ∈ s) ↔ ∃ ι (hι : Nonempty ι) (f : ι → Ordinal), (∀ i, f i ∈ s) ∧ ⨆ i, f i = a$$

Lean4

theorem mem_iff_iSup_of_isClosed (hs : IsClosed s) :
    a ∈ s ↔ ∃ (ι : Type u) (_hι : Nonempty ι) (f : ι → Ordinal), (∀ i, f i ∈ s) ∧ ⨆ i, f i = a := by
  rw [← mem_closure_iff_iSup, hs.closure_eq]

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