English
Two families of ordinals with the same target ordinal have equal iSup when indexed by isomorphic well-orders.
Русский
Две семейства ординалов с одинаковым целевым ординалом имеют равный iSup, когда индексируются по изоморфным хорошо упорядоченным множествам.
LaTeX
$$$$ \\mathrm{iSup}\\big( \\operatorname{familyOfBFamily'}(r,ho,f) \\big) = \\mathrm{iSup}\\big( \\operatorname{familyOfBFamily'}(r',ho',f) \\big) $$$$
Lean4
theorem iSup_eq_iSup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r']
{o : Ordinal} (ho : type r = o) (ho' : type r' = o) (f : ∀ a < o, Ordinal) :
iSup (familyOfBFamily' r ho f) = iSup (familyOfBFamily' r' ho' f) :=
iSup_eq_of_range_eq (by simp)
