thickening_eq_empty_iff_of_pos

Mathlib.Topology.MetricSpace.Thickening

URI: https://scilib.ai/kg/mathlib#Metric.thickening_eq_empty_iff_of_pos

← MathLib Explorer

English

If ε > 0, thickening ε s = ∅ if and only if s = ∅.

Русский

Если ε > 0, то thickening ε s = ∅ тогда и только тогда, когда s = ∅.

LaTeX

$$$\\mathrm{thickening}_{\\varepsilon}(s) = \\emptyset \\iff \\varepsilon > 0$ и $s = \\emptyset$.$$

Lean4

theorem thickening_eq_empty_iff_of_pos (hε : 0 < ε) : thickening ε s = ∅ ↔ s = ∅ :=
  ⟨fun h ↦ subset_eq_empty (self_subset_thickening hε _) h, by simp +contextual⟩

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

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

Разделы

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

Аффилиация

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