bsup_eq_bsup — Mathlib

English

If two orders r and r' are well-orders, then their bsups with the same f agree.

Русский

Если r и r' — хорошие упорядочения, то их bsup с тем же f совпадают.

LaTeX

$$$$ (r, r') \\text{ well-orders} \\Rightarrow \\mathrm{bsup}'(r,f) = \\mathrm{bsup}'(r',f) $$$$

Lean4

theorem bsup_eq_bsup {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r']
    (f : ι → Ordinal.{max u v}) : bsup.{_, v} _ (bfamilyOfFamily' r f) = bsup.{_, v} _ (bfamilyOfFamily' r' f) := by
  rw [bsup'_eq_iSup, bsup'_eq_iSup]

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