bsup_one

Mathlib.SetTheory.Ordinal.Family

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

← MathLib Explorer

English

Over the domain 1, bsup reduces to the single evaluation f(0, 0<1).

Русский

На домене 1 bsup равно единственному значению f(0, 0<1).

LaTeX

$$$\\operatorname{bsup}(1, f) = f(0, 0 < 1)$$$

Lean4

@[simp]
theorem bsup_one (f : ∀ a < (1 : Ordinal), Ordinal) : bsup 1 f = f 0 zero_lt_one := by
  simp_rw [← iSup_eq_bsup, ciSup_unique, familyOfBFamily, familyOfBFamily', typein_one_toType]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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