English
If two well-orders r and r' on types ι and ι' correspond to the same ordinal o, then lsub of the corresponding bi-families are equal.
Русский
Если два хорошо упорядоченных отношения приводят к одному ординалу o, то lsub соответствующих би-семейств равен.
LaTeX
$$$\operatorname{lsub}(\text{familyOfBFamily'}\, r\, ho\, f) = \operatorname{lsub}(\text{familyOfBFamily'}\, r'\, ho'\, f)$$$
Lean4
theorem lsub_eq_lsub {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o}
(ho : type r = o) (ho' : type r' = o) (f : ∀ a < o, Ordinal.{max u v}) :
lsub.{_, v} (familyOfBFamily' r ho f) = lsub.{_, v} (familyOfBFamily' r' ho' f) := by
rw [lsub_eq_blsub', lsub_eq_blsub']
