inf_strictMonoOn_Icc_sup — Mathlib

English

For any a,b in a modular lattice, the map c ↦ a ∧ c is strictly monotone on the interval Icc(b, a ∨ b).

Русский

Для любых a,b в модульной решётке отображение c ↦ a ∧ c строго возрастает на промежутке Icc(b, a ∨ b).

LaTeX

$$$\text{StrictMonoOn}(\lambda c\, , a\wedge c)\, (Icc\, b\, (a\vee b)).$$$

Lean4

theorem inf_strictMonoOn_Icc_sup {a b : α} : StrictMonoOn (fun c => a ⊓ c) (Icc b (a ⊔ b)) :=
  StrictMono.of_restrict (infIccOrderIsoIccSup a b).symm.strictMono

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