right_lt_sup

Mathlib.Order.Lattice

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

English

Let α be a join-semilattice and a,b ∈ α. Then b < a ⊔ b iff ¬(a ≤ b).

Русский

Пусть α — полусуплей, для любых a, b ∈ α верно: b < a ⊔ b эквивалентно не (a ≤ b).

LaTeX

$$$b < a \sqcup b \leftrightarrow a \nle b$$$

Lean4

@[simp]
theorem right_lt_sup : b < a ⊔ b ↔ ¬a ≤ b :=
  le_sup_right.lt_iff_ne.trans <| not_congr right_eq_sup

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

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

Разделы

Аффилиация

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