blsub_eq_lsub' — Mathlib

English

Characterizes when blsub o f ≤ a in terms of all i<h and a bound on f i h.

Русский

Характеризуется тем, что blsub o f ≤ a эквивалентно тому, что для всех i,h выполняется f i h ≤ a.

LaTeX

$$$\blsub o f ≤ a \iff \forall i,h, f i h ≤ a$$$

Lean4

@[simp]
theorem blsub_eq_lsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u v}) :
    blsub.{_, v} _ (bfamilyOfFamily' r f) = lsub.{_, v} f :=
  bsup'_eq_iSup r (succ ∘ f)

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