codRestrict — Mathlib

English

If f is strictly monotone and every x maps into a set s, then the codRestrict of f to s is strictly monotone.

Русский

Если f строго монотонна и изображение f лежит в s, то codRestrict f s строго монотонна.

LaTeX

$$$\text{StrictMono}(f) \to \forall x, f(x) \in s \Rightarrow \operatorname{StrictMono}(\operatorname{Set.codRestrict} f s hs)$$$

Lean4

theorem codRestrict (hf : StrictMono f) {s : Set β} (hs : ∀ x, f x ∈ s) : StrictMono (Set.codRestrict f s hs) :=
  hf

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