eq_of_le_of_inf_le_of_le_sup — Mathlib

English

If x ≤ y, y ⊓ z ≤ x, and y ≤ x ⊔ z in a modular lattice, then x = y.

Русский

Если x ≤ y, y ⊓ z ≤ x и y ≤ x ⊔ z в модульной решётке, то x = y.

LaTeX

$$$ x \\le y \\land y \\land z \\le x \\land y \\le x \\lor z \\Rightarrow x = y $$$

Lean4

theorem eq_of_le_of_inf_le_of_le_sup (hxy : x ≤ y) (hinf : y ⊓ z ≤ x) (hsup : y ≤ x ⊔ z) : x = y :=
  by
  refine hxy.antisymm ?_
  rw [← inf_eq_right, sup_inf_assoc_of_le _ hxy] at hsup
  rwa [← hsup, sup_le_iff, and_iff_right rfl.le, inf_comm]

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