empty_left

Mathlib.Topology.MetricSpace.MetricSeparated

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

English

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

Русский

Левая часть ε-разделена от пустого множества: AreSeparated(ε, ∅).

LaTeX

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

Lean4

@[simp]
theorem empty_left (s : Set X) : AreSeparated ∅ s :=
  ⟨1, one_ne_zero, fun _x => False.elim⟩

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

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

Разделы

Аффилиация

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