strictMono_inf_prod_sup — Mathlib

English

Let α be a modular lattice and fix z ∈ α. The map x ↦ (x ∧ z, x ∨ z) from α to α × α is strictly monotone with respect to the product order; in particular, whenever x < y we have (x ∧ z, x ∨ z) < (y ∧ z, y ∨ z).

Русский

Пусть α — модульная решетка и зафиксируем z ∈ α. Функция x ↦ (x ∧ z, x ∨ z) из α в α × α строго возрастает по отношению к произведению порядков; более точно, если x < y, то (x ∧ z, x ∨ z) < (y ∧ z, y ∨ z).

LaTeX

$$$\forall x,y,z\in \alpha\,(x

Lean4

theorem strictMono_inf_prod_sup : StrictMono fun x ↦ (x ⊓ z, x ⊔ z) := fun _x _y hxy ↦
  ⟨⟨inf_le_inf_right _ hxy.le, sup_le_sup_right hxy.le _⟩, fun ⟨inf_le, sup_le⟩ ↦
    (sup_lt_sup_of_lt_of_inf_le_inf hxy inf_le).not_ge sup_le⟩

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