bsup_le_blsub — Mathlib

English

Let o be an ordinal and f a function defined on the set {a : a < o} taking values in ordinals. Then the b-supremum of f over a < o is bounded above by the b-l-sub of f, i.e. bsup(o, f) ≤ blsub(o, f).

Русский

Пусть o — ординал, а f — функция, определённая на множествах {a : a < o}, принимающая значения в ординалах. Тогда b-супремум f над a < o не превышает b-l-sub f: bsup(o, f) ≤ blsub(o, f).

LaTeX

$$$\forall o:\,\mathrm{Ord},\ f:\{a

Lean4

theorem bsup_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : bsup.{_, v} o f ≤ blsub.{_, v} o f :=
  bsup_le fun i h => (lt_blsub f i h).le

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