bfamilyOfFamily — Mathlib

English

A version of bfamilyOfFamily' that maps a source to a target via a type-indexed family with an IsWellOrder structure.

Русский

Версия функции bfamilyOfFamily', переводящая источник в цель через семейство по типу с структурой IsWellOrder.

LaTeX

$$$ {ι : Type} (r : ι \to ι \to Prop) [IsWellOrder ι r] \to (f : ι \to α) \to (a : Ordinal) \to (a < type r) \to α $$$

Lean4

/-- Converts a family indexed by a `Type u` to one indexed by an `Ordinal.{u}` using a well-ordering
given by the axiom of choice. -/
def bfamilyOfFamily {ι : Type u} : (ι → α) → ∀ a < type (@WellOrderingRel ι), α :=
  bfamilyOfFamily' WellOrderingRel

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