edist_mul_mul_le — Mathlib

English

Let E be a seminormed commutative group. For all a1, a2, b1, b2 in E, edist(a1 a2, b1 b2) ≤ edist(a1, b1) + edist(a2, b2).

Русский

Пусть E — полугруппа с нормой. Для любых a1, a2, b1, b2 ∈ E выполняется edist(a1 a2, b1 b2) ≤ edist(a1, b1) + edist(a2, b2).

LaTeX

$$$\\forall a_1,a_2,b_1,b_2\\in E:\\; \\mathrm{edist}(a_1 a_2, b_1 b_2) \\le \\mathrm{edist}(a_1,b_1) + \\mathrm{edist}(a_2,b_2).$$$

Lean4

@[to_additive]
theorem edist_mul_mul_le (a₁ a₂ b₁ b₂ : E) : edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂ :=
  by
  simp only [edist_nndist]
  norm_cast
  apply nndist_mul_mul_le

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