restrict_iff — Mathlib

English

The Hölder-on-restricted-function property on s is equivalent to the Hölder-on-with property of the original function on s.

Русский

Свойство Холдер-на-ограниченной-функции на s эквивалентно свойству Холдер-на-с-отдельно для исходной функции на s.

LaTeX

$$$\operatorname{HolderWith}(C,r,f|_{s}) \;\iff\; \operatorname{HolderOnWith}(C,r,f,s)$$$

Lean4

theorem restrict_iff {s : Set X} : HolderWith C r (s.restrict f) ↔ HolderOnWith C r f s := by
  simp [HolderWith, HolderOnWith]

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