sub_ne_top_iff

Mathlib.Data.ENat.Basic

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

English

a - b ≠ ⊤ iff a ≠ ⊤ ∨ b = ⊤.

Русский

a - b ≠ ⊤ тогда и только тогда a ≠ ⊤ или b = ⊤.

LaTeX

$$$a - b \neq \top \iff a \neq \top \lor b = \top$$$

Lean4

theorem sub_ne_top_iff : a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤ :=
  WithTop.sub_ne_top_iff

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

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

Разделы

Аффилиация

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