monotoneOn — Mathlib

English

If s is a subsingleton, then any function f is monotone on s; i.e., for all a,b ∈ s with a ≤ b we have f(a) ≤ f(b).

Русский

Если s является пододиноством, то любая функция f монотонна на s: для любых a,b ∈ s, если a ≤ b, то f(a) ≤ f(b).

LaTeX

$$$ \forall x \in s, \forall y \in s, x \le y \Rightarrow f(x) \le f(y)$$$

Lean4

protected theorem monotoneOn (h : s.Subsingleton) : MonotoneOn f s := fun _ ha _ hb _ => (congr_arg _ (h ha hb)).le

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