continuous_edist — Mathlib

English

The edist map on a product or pair is continuous in each argument.

Русский

Функция edist непрерывна по каждому аргументу пары.

LaTeX

$$$\text{Continuous }(p \mapsto \mathrm{edist}(p_1,p_2))$ for suitable spaces.$$

Lean4

theorem continuous_edist : Continuous fun p : α × α => edist p.1 p.2 :=
  by
  apply continuous_of_le_add_edist 2 (by decide)
  rintro ⟨x, y⟩ ⟨x', y'⟩
  calc
    edist x y ≤ edist x x' + edist x' y' + edist y' y := edist_triangle4 _ _ _ _
    _ = edist x' y' + (edist x x' + edist y y') := by simp only [edist_comm]; ac_rfl
    _ ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) := by
      gcongr <;> apply_rules [le_max_left, le_max_right]
    _ = edist x' y' + 2 * edist (x, y) (x', y') := by rw [← mul_two, mul_comm]

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