blsub_eq_zero_iff

Mathlib.SetTheory.Ordinal.Family

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

← MathLib Explorer

English

blsub o f equals 0 if and only if o equals 0.

Русский

blsub o f равно 0 тогда, когда o = 0.

LaTeX

$$$ \\operatorname{blsub}(o,f) = 0 \\iff o = 0 $$$

Lean4

@[simp]
theorem blsub_eq_zero_iff {o} {f : ∀ a < o, Ordinal} : blsub o f = 0 ↔ o = 0 :=
  by
  rw [← lsub_eq_blsub, lsub_eq_zero_iff]
  exact toType_empty_iff_eq_zero

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

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

Разделы

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

Аффилиация

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