inf_lt_sup

Mathlib.Order.Lattice

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

English

In a lattice, a ∧ b is strictly less than a ∨ b if and only if a ≠ b.

Русский

В решётке инфимум двух элементов строго меньше их супремума тогда и только тогда, когда элементы различны.

LaTeX

$$$a \wedge b < a \vee b \iff a \neq b$$$

Lean4

@[simp]
theorem inf_lt_sup : a ⊓ b < a ⊔ b ↔ a ≠ b := by rw [inf_le_sup.lt_iff_ne, Ne, inf_eq_sup]

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

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

Разделы

Аффилиация

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