restrict — Mathlib

English

If f is monotone, then restricting its domain to a subset s yields a monotone function on s.

Русский

Если f монотонна, то ограничение области определения до подмножества s даёт монотонную функцию на s.

LaTeX

$$$\text{Monotone}(f) \Rightarrow \forall s, \operatorname{Monotone}(s.restrict f)$$$

Lean4

protected theorem restrict (h : Monotone f) (s : Set α) : Monotone (s.restrict f) := fun _ _ hxy => h hxy

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