lt_iff_le_and_ne

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#lt_iff_le_and_ne

English

a < b iff a ≤ b and a ≠ b.

Русский

a < b тогда и только тогда, когда a ≤ b и a ≠ b.

LaTeX

$$$ a < b \iff a \le b \land a \neq b $$$

Lean4

theorem lt_iff_le_and_ne : a < b ↔ a ≤ b ∧ a ≠ b :=
  ⟨fun h ↦ ⟨le_of_lt h, ne_of_lt h⟩, fun ⟨h1, h2⟩ ↦ h1.lt_of_ne h2⟩

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

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

Разделы

Аффилиация

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