English
If α is well-ordered by r, then blsub over type r corresponds to lsub over a mapped index.
Русский
Пусть α хорошо упорядочено по r; тогда Blsub над типом r эквивалентен Lsub над индексированным отображением.
LaTeX
$$$ {\\alpha} : Type^u,\\ r : \\alpha \\to \\alpha \\to Prop,\\ f : ∀ a < type(r), Ordinal \\\\blsub_{v} (type\\ r)\\ f = \\operatorname{lsub}(\\lambda a. f (typein\\ r\\ a) (typein\\lt\\type r\\ a)) $$$
Lean4
theorem blsub_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : ∀ a < type r, Ordinal.{max u v}) :
blsub.{_, v} (type r) f = lsub.{_, v} fun a => f (typein r a) (typein_lt_type _ _) :=
eq_of_forall_ge_iff fun o => by
rw [blsub_le_iff, lsub_le_iff]
exact ⟨fun H b => H _ _, fun H i h => by simpa only [typein_enum] using H (enum r ⟨i, h⟩)⟩
