untop₀_eq_zero

Mathlib.Algebra.Order.WithTop.Untop0

URI: https://scilib.ai/kg/mathlib#WithTop.untop₀_eq_zero

English

For any element a in WithTop α, we have a.untop₀ = 0 iff a = 0 or a = ⊤.

Русский

Для любого элемента a из WithTop α выполняется a.untop₀ = 0 тогда и только тогда, когда a = 0 или a = ⊤.

LaTeX

$$$a.untop_0 = 0 \iff a = 0 \lor a = \top$$$

Lean4

@[simp]
theorem untop₀_eq_zero {a : WithTop α} : a.untop₀ = 0 ↔ a = 0 ∨ a = ⊤ := by simp [untop₀]

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

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

Разделы

Аффилиация

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