bsup_congr — Mathlib

English

Another variant stating equality of bsup for two well-orders.

Русский

Еще один вариант утверждает равенство bsup для двух хорошо упорядоченных множеств.

LaTeX

$$$$ (r,r') \\text{ WellOrder} \\Rightarrow \\mathrm{bsup}(r,f) = \\mathrm{bsup}(r',f) $$$$

Lean4

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

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