monotoneOn_iff_monotone — Mathlib

English

Let f: α → β and s ⊆ α. Then f is monotone on s if and only if the restricted map a ↦ f(a) on s is monotone: MonotoneOn f s ⇔ Monotone (λ a : s. f(a)).

Русский

Пусть f: α → β и s ⊆ α. Тогда f монотонна на s тогда и только тогда ограниченная функция a ↦ f(a) на s монотонна: MonotoneOn f s ⇔ Monotone (λ a : s. f(a)).

LaTeX

$$$ \operatorname{MonotoneOn}(f,s) \iff \operatorname{Monotone}(\lambda a : s. f(a))$$$

Lean4

theorem monotoneOn_iff_monotone : MonotoneOn f s ↔ Monotone fun a : s => f a := by simp [Monotone, MonotoneOn]

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