mono — Mathlib

English

Let f be an element of CircleDeg1Lift. Then f is order-preserving: for all x ≤ y (with x,y ∈ ℝ), f(x) ≤ f(y).

Русский

Пусть f принадлежит CircleDeg1Lift. Тогда отображение монотонно по порядку: для любых x ≤ y (x,y ∈ ℝ) выполняется f(x) ≤ f(y).

LaTeX

$$$\\forall f \\in CircleDeg1Lift,\\ \\forall x,y \\in \\mathbb{R},\\ x \\le y \\Rightarrow f x \\le f y$$$

Lean4

@[mono]
theorem mono {x y} (h : x ≤ y) : f x ≤ f y :=
  f.monotone h

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