mem_closure_iff_bsup — Mathlib

English

a ∈ closure s iff there exists an o ≠ 0 and f with a-bounded bsup representation within s.

Русский

a ∈ closure s эквивалентно существованию o ≠ 0 и f: ∀ x < o, Ordinal, такая что a = bsup o f и f описывает элементы из s.

LaTeX

$$$a \in \overline{s} \iff \exists o \; (o \neq 0) \; \exists f : \forall x < o, Ordinal, (\forall i < o, f i < o) \land \text{bsup}(o,f) = a$$$

Lean4

theorem mem_closure_iff_bsup :
    a ∈ closure s ↔ ∃ (o : Ordinal) (_ho : o ≠ 0) (f : ∀ a < o, Ordinal), (∀ i hi, f i hi ∈ s) ∧ bsup.{u, u} o f = a :=
  by
  apply ((mem_closure_tfae a s).out 0 4).trans
  simp_rw [exists_prop]

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