empty_right

Mathlib.Topology.MetricSpace.MetricSeparated

URI: https://scilib.ai/kg/mathlib#Metric.AreSeparated.empty_right

English

The right side is ε-separated from the empty set: AreSeparated(ε, ∅) via symmetry.

Русский

Правая часть ε-разделена от пустого множества; следует из симметрии.

LaTeX

$$$\\operatorname{AreSeparated}(\\varepsilon, \\varnothing)$$$

Lean4

@[simp]
theorem empty_right (s : Set X) : AreSeparated s ∅ :=
  (empty_left s).symm

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

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

Разделы

Аффилиация

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