Theorems · Theorem · logic and foundations

Ordinal.mem_closure_tfae

∀ (a : Ordinal.{u}) (s : Set Ordinal.{u}),
  [a ∈ closure s, a ∈ closure (s ∩ Set.Iic a), (s ∩ Set.Iic a).Nonempty ∧ sSup (s ∩ Set.Iic a) = a,
      ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE

Defined in

Mathlib.SetTheory.Ordinal.Topology

Cited by

1 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound