lt_top_iff_ne_top

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.lt_top_iff_ne_top

← MathLib Explorer

English

For x ∈ WithTop(α), x < ⊤ iff x ≠ ⊤.

Русский

Для любого x ∈ WithTop(α) верно: x < ⊤ тогда как x ≠ ⊤.

LaTeX

$$$$ x < \\top \\;\\iff\\; x \\neq \\top. $$$$

Lean4

/-- A version of `lt_top_iff_ne_top` for `WithTop` that only requires `LT α`, not
`PartialOrder α`. -/
protected theorem lt_top_iff_ne_top : x < ⊤ ↔ x ≠ ⊤ := by cases x <;> simp

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

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

Разделы

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

Аффилиация

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