le_mul_norm_div — Mathlib

English

If f is AntilipschitzWith K, then for all x,y in E, ||x/y|| ≤ K * ||f(x)/f(y)||.

Русский

Если f — антилипшицев с константой K, то для любых x,y ∈ E выполняется ||x/y|| ≤ K · ||f(x)/f(y)||.

LaTeX

$$$\\forall x,y\\in E:\\; \\|\\frac{x}{y}\\| \\le K \\cdot \\big\\|\\frac{f(x)}{f(y)}\\big\\|.$$$

Lean4

@[to_additive le_mul_norm_sub]
theorem le_mul_norm_div {f : E → F} (hf : AntilipschitzWith K f) (x y : E) : ‖x / y‖ ≤ K * ‖f x / f y‖ := by
  simp [← dist_eq_norm_div, hf.le_mul_dist x y]

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