thickening_nonempty_iff

Mathlib.Topology.MetricSpace.Thickening

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

English

The thickening is nonempty if and only if ε > 0 and s is nonempty.

Русский

Утолщение непусто тогда, когда ε > 0 и s непусто.

LaTeX

$$$\\mathrm{thickening}_{\\varepsilon}(s).\\text{Nonempty} \\iff 0 < \\varepsilon \\wedge s.\\text{Nonempty}$$$

Lean4

@[simp]
theorem thickening_nonempty_iff : (thickening ε s).Nonempty ↔ 0 < ε ∧ s.Nonempty := by simp [nonempty_iff_ne_empty]

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

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

Разделы

Аффилиация

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