lsub_eq_blsub' — Mathlib

English

Under appropriate well-ordering data, lsub of the bfamily' equals blsub.

Русский

При разумном выборе упорядования, lsub(bfamily') = blsub.

LaTeX

$$$\operatorname{lsub}(\text{familyOfBFamily'}\, r\, ho\, f) = \operatorname{blsub}(o\, f)$$$

Lean4

theorem lsub_eq_blsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} (ho : type r = o) (f : ∀ a < o, Ordinal) :
    lsub (familyOfBFamily' r ho f) = blsub o f :=
  iSup'_eq_bsup r ho fun a ha => succ (f a ha)

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