thickening_empty

Mathlib.Topology.MetricSpace.Thickening

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

← MathLib Explorer

English

The thickening of the empty set is empty: thickening δ ∅ = ∅.

Русский

Уплотнение пустого множества равно пустому: thickening δ ∅ = ∅.

LaTeX

$$$thickening\\,δ\\,(∅) = ∅$$$

Lean4

/-- The (open) thickening of the empty set is empty. -/
@[simp]
theorem thickening_empty (δ : ℝ) : thickening δ (∅ : Set α) = ∅ := by
  simp only [thickening, setOf_false, infEdist_empty, not_top_lt]

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

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

Разделы

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

Аффилиация

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