instIsTopologicalAddTorsor_1 — Mathlib

English

For p1,p2,p3,p4 ∈ P, edist(p1 −ᵥ p2, p3 −ᵥ p4) ≤ edist(p1,p3) + edist(p2,p4).

Русский

Пусть p1,p2,p3,p4 ∈ P. edist(p1 −ᵥ p2, p3 −ᵥ p4) ≤ edist(p1,p3) + edist(p2,p4).

LaTeX

$$$\operatorname{edist}(p_1 -ᵥ p_2, p_3 -ᵥ p_4) \le \operatorname{edist}(p_1,p_3) + \operatorname{edist}(p_2,p_4)$$$

Lean4

instance : IsTopologicalAddTorsor P
    where
  continuous_vadd := uniformContinuous_vadd.continuous
  continuous_vsub := uniformContinuous_vsub.continuous

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