sub_ne_top_iff

Mathlib.Algebra.Order.Sub.WithTop

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

English

In WithTop α, a − b ≠ ⊤ iff a ≠ ⊤ or b = ⊤.

Русский

В WithTop α, a − b ≠ ⊤ тогда и только тогда, когда a ≠ ⊤ или b = ⊤.

LaTeX

$$$\forall a,b \in WithTop \alpha\,(a - b \neq \top) \iff (a \neq \top \lor b = \top)$$$

Lean4

theorem sub_ne_top_iff {a b : WithTop α} : a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤ := by simp [or_iff_not_imp_left]

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

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

Разделы

Аффилиация

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