dist_norm_norm_le' — Mathlib

English

Let E be a seminormed group. For all a, b in E, the distance between their norms satisfies dist(||a||, ||b||) ≤ ||a / b||.

Русский

Пусть E — полугруппа с полем нормы. Для любых a, b ∈ E выполняется неравенство расстояния между нормами: dist(||a||, ||b||) ≤ ||a / b||.

LaTeX

$$$$ \operatorname{dist} (\|a\|, \|b\|) \le \|a / b\|. $$$$

Lean4

@[to_additive dist_norm_norm_le]
theorem dist_norm_norm_le' (a b : E) : dist ‖a‖ ‖b‖ ≤ ‖a / b‖ :=
  abs_norm_sub_norm_le' a b

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