brange

Mathlib.SetTheory.Ordinal.Family

URI: https://scilib.ai/kg/mathlib#Ordinal.brange

English

The range of a family indexed by an ordinal is the set of all its values.

Русский

Диапазон семейства, индексируемого по порядковым числам, состоит из всех значений семейства.

LaTeX

$$$\mathrm{brange}(o,f) = \{ a \mid \exists i

Lean4

/-- The range of a family indexed by ordinals. -/
def brange (o : Ordinal) (f : ∀ a < o, α) : Set α :=
  {a | ∃ i hi, f i hi = a}

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru