blsub_congr — Mathlib

English

Relates the order-theoretic comparison between a and blsub o f to existence of an index witnessing bound.

Русский

Связь между сравнением a и o.blsub f и существованием индекса, доказывающего предел.

LaTeX

$$$a < o.blsub f \iff \exists i, hi, a \le f(i,hi)$$$

Lean4

@[congr]
theorem blsub_congr {o₁ o₂ : Ordinal.{u}} (f : ∀ a < o₁, Ordinal.{max u v}) (ho : o₁ = o₂) :
    blsub.{_, v} o₁ f = blsub.{_, v} o₂ fun a h => f a (h.trans_eq ho.symm) :=
  by
  subst ho
  rfl

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