codRestrict — Mathlib

English

If f is monotone and its image lies in a set s, then the codomain restriction s codRestrict f is monotone.

Русский

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

LaTeX

$$$\operatorname{Monotone}(f) \Rightarrow \forall s, (\forall x, f(x)\in s) \Rightarrow \operatorname{Monotone}(\operatorname{Set.codRestrict} f s \; )$$$

Lean4

protected theorem codRestrict (h : Monotone f) {s : Set β} (hs : ∀ x, f x ∈ s) : Monotone (s.codRestrict f hs) :=
  h

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