mem_closure_iff_iSup — Mathlib

English

a ∈ closure s iff there exists an index type ι, a nonempty, a function f: ι → Ordinal with f(i) ∈ s for all i and ⨆_i f(i) = a.

Русский

a ∈ closure s эквивалентно существованию типа ι, не пустого, функции f: ι → Ordinal такая, что для всех i f(i) ∈ s и ⨆_i f(i) = a.

LaTeX

$$$a \in \overline{s} \iff \exists ι (hι : Nonempty ι) (f : ι \to Ordinal), (\forall i, f(i) \in s) \wedge \big\langle i, \text{?} \big\rangle = a$$$

Lean4

theorem mem_closure_iff_iSup :
    a ∈ closure s ↔ ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal), (∀ i, f i ∈ s) ∧ ⨆ i, f i = a :=
  by
  apply ((mem_closure_tfae a s).out 0 5).trans
  simp_rw [exists_prop]

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