symm — Mathlib

English

AreSeparated is symmetric: if s is ε-separated from t, then t is ε-separated from s.

Русский

Разделённость симметрична: если s ε-разделено от t, то t ε-разделено от s.

LaTeX

$$$\\operatorname{AreSeparated}(s,t) \\Rightarrow \\operatorname{AreSeparated}(t,s)$$$

Lean4

@[symm]
theorem symm (h : AreSeparated s t) : AreSeparated t s :=
  let ⟨r, r0, hr⟩ := h
  ⟨r, r0, fun y hy x hx => edist_comm x y ▸ hr x hx y hy⟩

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