range_familyOfBFamily

Mathlib.SetTheory.Ordinal.Family

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

English

The range of the canonical BFamily equals the brange of f.

Русский

Диапазон канонического BFAMILY равен brange f.

LaTeX

$$$\mathrm{range}(\mathrm{familyOfBFamily}(o,f)) = \mathrm{brange}(o,f)$$$

Lean4

@[simp]
theorem range_familyOfBFamily {o} (f : ∀ a < o, α) : range (familyOfBFamily o f) = brange o f :=
  range_familyOfBFamily' _ _ f

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

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

Разделы

Аффилиация

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