monotone — Mathlib

English

Let l be a LowerAdjoint of u; then the composition u ∘ l is monotone: for all a, b ∈ α, if a ≤ b then u(l(a)) ≤ u(l(b)).

Русский

Пусть l — нижнее сопряжение к u; тогда композиция u ∘ l монотонна: для любых a, b ∈ α, если a ≤ b, то u(l(a)) ≤ u(l(b)).

LaTeX

$$$\\forall a,b \\in \\alpha,\\ a \\le b \\Rightarrow u(l(a)) \\le u(l(b))$$$

Lean4

@[mono]
theorem monotone : Monotone (u ∘ l) :=
  l.gc.monotone_u.comp l.gc.monotone_l

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