antilipschitzWith_inv_iff — Mathlib

English

For an inverse map f⁻¹ to be antilipschitz with constant K, the original map f must be antilipschitz with the same constant, i.e., f⁻¹ is K-Antilipschitz iff f is K-Antilipschitz.

Русский

Обратное отображение f^{-1} является антилипшицевым с константой K тогда и только тогда, когда сама функция f является антилипшицевой с константой K.

LaTeX

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

Lean4

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

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