iSup_eq_bsup

Mathlib.SetTheory.Ordinal.Family

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

English

For a well-ordered index, bsup' equals iSup when applied to the appropriate bfamily.

Русский

Для упорядоченного индекса bsup' равен iSup при применении соответствующего bfamily.

LaTeX

$$$$ \\operatorname{bsup}'(r) = \\mathrm{iSup} \\big( \\mathrm{bfamilyOfFamily'}(r, f) \\big) $$$$

Lean4

@[simp]
theorem iSup_eq_bsup {o : Ordinal} (f : ∀ a < o, Ordinal) : iSup (familyOfBFamily o f) = bsup o f :=
  rfl

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

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

Разделы

Аффилиация

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