left_lt_sup — Mathlib

English

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

Русский

Пусть α — полусплошенная полупорядованная множество с операцией объединения ⊔. Для любых a, b ∈ α верно: a < a ⊔ b тогда и только тогда, когда не выполняется b ≤ a.

LaTeX

$$$a < a \sqcup b \leftrightarrow \neg (b \le a)$$$

Lean4

@[simp]
theorem left_lt_sup : a < a ⊔ b ↔ ¬b ≤ a :=
  le_sup_left.lt_iff_ne.trans <| not_congr left_eq_sup

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