English
Let o be an ordinal and f assign to each a < o an element of α. Then there is a canonical reindexed family defined on the type o that encodes the same data via the fixed well-ordering of o.
Русский
Пусть o — порядковый множитель и d задаёт элемент α для каждого a < o. Тогда существует каноническое переиндексирование семейства, определённое на типе o, которое кодирует те же данные через заданное хорошо упорядочение o.
LaTeX
$$$\mathrm{familyOfBFamily}(o,f) : o.\mathrm{toType} \to \alpha$$$
Lean4
/-- Converts a family indexed by an `Ordinal.{u}` to one indexed by a `Type u` using a well-ordering
given by the axiom of choice. -/
def familyOfBFamily (o : Ordinal) (f : ∀ a < o, α) : o.toType → α :=
familyOfBFamily' (· < ·) (type_toType o) f
