bfamilyOfFamily' — Mathlib

English

Converts a family indexed by a Type to one indexed by an ordinal, using a specified well-ordering.

Русский

Преобразует семейство, индексируемое типом, в семейство, индексируемое ординалом, с использованием заданного хорошо упорядочения.

LaTeX

$$$ {ι : Type} \to {α},\; \text{IsWellOrder }ι r \Rightarrow \text{bfamilyOfFamily'}(r,f) $$

Lean4

/-- Converts a family indexed by a `Type u` to one indexed by an `Ordinal.{u}` using a specified
well-ordering. -/
def bfamilyOfFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) : ∀ a < type r, α := fun a ha =>
  f (enum r ⟨a, ha⟩)

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