sup_lt_sup_of_lt_of_inf_le_inf — Mathlib

English

In a modular lattice, if x < y and y ∧ z ≤ x ∧ z, then x ∨ z < y ∨ z.

Русский

В модульной решётке, если x < y и y ∧ z ≤ x ∧ z, тогда x ∨ z < y ∨ z.

LaTeX

$$$ h_{xy} : x < y, \\; hinf : y \\land z \\le x \\land z \\Rightarrow x \\lor z < y \\lor z $$$

Lean4

theorem sup_lt_sup_of_lt_of_inf_le_inf (hxy : x < y) (hinf : y ⊓ z ≤ x ⊓ z) : x ⊔ z < y ⊔ z :=
  lt_of_le_of_ne (sup_le_sup_right (le_of_lt hxy) _) fun hsup =>
    ne_of_lt hxy <| eq_of_le_of_inf_le_of_sup_le (le_of_lt hxy) hinf (le_of_eq hsup.symm)

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