strictMonoOn_iff_strictMono — Mathlib

English

Let f: α → β and s ⊆ α. Then f is strictly monotone on s iff the restricted map a ↦ f(a) on s is strictly monotone: StrictMonoOn f s ⇔ StrictMono (λ a : s. f(a)).

Русский

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

LaTeX

$$$ \operatorname{StrictMonoOn}(f,s) \iff \operatorname{StrictMono}(\lambda a : s. f(a))$$$

Lean4

theorem strictMonoOn_iff_strictMono : StrictMonoOn f s ↔ StrictMono fun a : s => f a := by
  simp [StrictMono, StrictMonoOn]

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