to_rightInverse — Mathlib

English

If f is Lipschitz with constant K and g is a right inverse of f (f ∘ g = id), then g is AntilipschitzWith K.

Русский

Если f — липшиц с постоянной K, и g является правым обратным к f (f ∘ g = id), тогда g — AntilipschitzWith K.

LaTeX

$$$ \text{LipschitzWith } K f \Rightarrow \forall g, (\text{RightInverse } g f) \Rightarrow \operatorname{AntilipschitzWith} K g$$$

Lean4

theorem to_rightInverse [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0} {f : α → β} (hf : LipschitzWith K f)
    {g : β → α} (hg : Function.RightInverse g f) : AntilipschitzWith K g := fun x y => by
  simpa only [hg _] using hf (g x) (g y)

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