dist_comm — Mathlib

English

For all x,y in the completion, dist x y = dist y x.

Русский

Для любых x,y из завершения dist x y = dist y x.

LaTeX

$$$\operatorname{dist} x y = \operatorname{dist} y x$$$

Lean4

protected theorem dist_comm (x y : Completion α) : dist x y = dist y x :=
  by
  refine induction_on₂ x y ?_ ?_
  ·
    exact
      isClosed_eq (Completion.continuous_dist continuous_fst continuous_snd)
        (Completion.continuous_dist continuous_snd continuous_fst)
  · intro a b
    rw [Completion.dist_eq, Completion.dist_eq, dist_comm]

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