mem_closedBall_comm — Mathlib

English

In a metric space, x belongs to the closed ball around y with radius ε if and only if y belongs to the closed ball around x with radius ε.

Русский

В метрическом пространстве верно, что x ∈ closedBall(y, ε) ⇔ y ∈ closedBall(x, ε).

LaTeX

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

Lean4

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

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