lipschitzOnWith_inv_iff — Mathlib

English

For any set s, if f is K-Lipschitz on s, then the inverse map f^{-1} is K-Lipschitz on s as a map from f(s) to the domain, and conversely.

Русский

Для множества s, если f ограниченно липшицево на s, то обратное отображение f^{-1} по области образа f(s) также липшицево с той же константой, и наоборот.

LaTeX

$$$\\mathrm{LipschitzOnWith}\\,K\\,f\\,s \\iff \\mathrm{LipschitzOnWith}\\,K\\,f^{-1}\\,s,$$$

Lean4

@[to_additive (attr := simp)]
theorem lipschitzOnWith_inv_iff : LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s := by simp [LipschitzOnWith]

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