sup_strictMonoOn_Icc_inf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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