isSymmetricRel_closedBall

Mathlib.Topology.MetricSpace.BundledFun

URI: https://scilib.ai/kg/mathlib#PseudoMetric.isSymmetricRel_closedBall

← MathLib Explorer

English

Similarly, the relation with distance at most ε is symmetric.

Русский

Аналогично, отношение с расстоянием не более ε симметрично.

LaTeX

$$$ IsSymmetricRel \{(x,y) \mid d(x,y) \le ε\}. $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru