mem_closedBall_comm — Mathlib

English

In a pseudo-EMetric space, x lies in the closed ball around y with radius ε if and only if y lies in the closed ball around x with radius ε.

Русский

В псевдосметрическом пространстве точка x принадлежит замкнутому шару вокруг y радиуса ε тогда и только тогда, когда y принадлежит замкнутому шару вокруг x радиуса ε.

LaTeX

$$$x \\in \\overline{B}(y,\\epsilon) \\iff y \\in \\overline{B}(x,\\epsilon)$$$

Lean4

theorem mem_closedBall_comm : x ∈ closedBall y ε ↔ y ∈ closedBall x ε := by rw [mem_closedBall', mem_closedBall]

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