right_lt_sup_of_left_ne_bot — Mathlib

English

If a and b are disjoint and a ≠ ⊥, then b < a ⊔ b in a semilattice with top and bottom.

Русский

Если a и b несовместимы и a ≠ ⊥, тогда b < a ⊔ b в полупредельной структуре с верхушкой и нулем.

LaTeX

$$$Disjoint\ a\ b \land a \neq \bot \Rightarrow b < a \lor b$$$

Lean4

theorem right_lt_sup_of_left_ne_bot [SemilatticeSup α] [OrderBot α] {a b : α} (h : Disjoint a b) (ha : a ≠ ⊥) :
    b < a ⊔ b :=
  le_sup_right.lt_of_ne fun eq ↦ ha (le_bot_iff.mp <| h le_rfl <| sup_eq_right.mp eq.symm)

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