lipschitzWith_inv_iff — Mathlib

English

For any α and E with a pseudo-metric structure, and any f: α → E, the map f is K-Lipschitz on its domain if and only if the inverse map f^{-1} (defined on the image f(α)) is K-Lipschitz.

Русский

Пусть имеется отображение f:α→E между метрическими пространствами; отображение f является K-Липшицевым на своей области тогда и только тогда, когда обратное отображение f^{-1}: f(α)→α является K-Липшицевым.

LaTeX

$$$\\forall K\\ge 0:\\; \\mathrm{LipschitzWith}\,K\\,f^{-1} \\;\\iff\\; \\mathrm{LipschitzWith}\,K\\,f,$$$

Lean4

@[to_additive (attr := simp)]
theorem lipschitzWith_inv_iff : LipschitzWith K f⁻¹ ↔ LipschitzWith K f := by simp [LipschitzWith]

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