completion_extension — Mathlib

English

If v1 ≅ v2 in the congruence relation, then v2 ≅ v1 (symmetry of the congruence).

Русский

Если v1 эквивален по отношению к конгруэнции с v2, то v2 эквивалентно v1 (симметричность).

LaTeX

$$$\text{Congruent } v_1\, v_2 \Rightarrow \text{Congruent } v_2\, v_1.$$$

Lean4

theorem completion_extension [MetricSpace β] [CompleteSpace β] {f : α → β} (h : Isometry f) :
    Isometry (Completion.extension f) :=
  Isometry.of_dist_eq fun x y =>
    induction_on₂ x y (isClosed_eq (by fun_prop) (by fun_prop)) fun _ _ ↦ by
      simp only [extension_coe h.uniformContinuous, Completion.dist_eq, h.dist_eq]

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