bsup_eq_blsub_or_succ_bsup_eq_blsub

English

For any o and function f, either bsup o f equals blsub o f, or succ(bsup o f) equals blsub o f.

Русский

Для любого ординала o и функции f либо bsup o f равен blsub o f, либо succ(bsup o f) равен blsub o f.

LaTeX

$$$ \\operatorname{bsup}(o,f) = \\operatorname{blsub}(o,f) \\quad \\lor \\quad \\operatorname{succ}(\\operatorname{bsup}(o,f)) = \\operatorname{blsub}(o,f) $$$

Lean4

theorem bsup_eq_blsub_or_succ_bsup_eq_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
    bsup.{_, v} o f = blsub.{_, v} o f ∨ succ (bsup.{_, v} o f) = blsub.{_, v} o f :=
  by
  rw [← iSup_eq_bsup, ← lsub_eq_blsub]
  exact iSup_eq_lsub_or_succ_iSup_eq_lsub _

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