isClosed_iff_bsup — Mathlib

English

IsClosed s iff for all o ≠ 0, all f : a < o → Ordinal with f(i) ∈ s, bsup o f ∈ s.

Русский

Замкнутость s эквивалентна тому, что для каждого o ≠ 0 и любой f : ∀ a < o, Ordinal с f(i) ∈ s, bsup o f ∈ s.

LaTeX

$$IsClosed s ↔ ∀ o ≠ 0 → ∀ f : ∀ a < o, Ordinal, (∀ i, f i ≤ s) → bsup(o,f) ∈ s$$

Lean4

theorem isClosed_iff_bsup :
    IsClosed s ↔ ∀ {o : Ordinal}, o ≠ 0 → ∀ f : ∀ a < o, Ordinal, (∀ i hi, f i hi ∈ s) → bsup.{u, u} o f ∈ s :=
  by
  rw [isClosed_iff_iSup]
  refine ⟨fun H o ho f hf => H (toType_nonempty_iff_ne_zero.2 ho) _ ?_, fun H ι hι f hf => ?_⟩
  · exact fun i => hf _ _
  · rw [← bsup_eq_iSup]
    apply H (type_ne_zero_iff_nonempty.2 hι)
    exact fun i hi =>
      hf
        _
          -- todo: generalize to other well-orders

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