isSymmetricRel_ball — Mathlib

English

For any Additive monoid with zero and a preorder, the set of pairs with distance less than ε is symmetric.

Русский

Для любого моноида с нулём и предела расстояние меньше чем ε образует симметричное отношение между точками.

LaTeX

$$$ IsSymmetricRel \{(x,y) \mid d(x,y) < \epsilon\}. $$$

Lean4

theorem isSymmetricRel_ball [Add R] [Zero R] [Preorder R] (d : PseudoMetric X R) {ε : R} :
    IsSymmetricRel {xy | d xy.1 xy.2 < ε} := by simp [IsSymmetricRel, d.symm]

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