restrict — Mathlib

English

If f contracts on s and MapsTo f s s, then the restricted map on s is contracting with the same constant.

Русский

Если f сжимает на s иMapsTo f s s, то ограничение на s сохраняет это свойство c той же константой.

LaTeX

$$$ \\text{ContractingWith } K\, f \\Rightarrow \\text{ContractingWith } K\\,(Set.MapsTo.restrict f\\, s\\, s)\\,.$$$

Lean4

/-- If a map `f` is `ContractingWith K`, and `s` is a forward-invariant set, then
restriction of `f` to `s` is `ContractingWith K` as well. -/
theorem restrict (hf : ContractingWith K f) {s : Set α} (hs : MapsTo f s s) : ContractingWith K (hs.restrict f s s) :=
  ⟨hf.1, fun x y ↦ hf.2 x y⟩

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