thickening_of_nonpos

Mathlib.Topology.MetricSpace.Thickening

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

← MathLib Explorer

English

If δ ≤ 0, then thickening δ E = ∅ for any E.

Русский

Если δ ≤ 0, то для любого E выполняется thickening δ E = ∅.

LaTeX

$$$δ ≤ 0 \\Rightarrow thickening\\,δ\\,E = ∅$$$

Lean4

theorem thickening_of_nonpos (hδ : δ ≤ 0) (s : Set α) : thickening δ s = ∅ :=
  eq_empty_of_forall_notMem fun _ => ((ENNReal.ofReal_of_nonpos hδ).trans_le bot_le).not_gt

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

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

Разделы

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

Аффилиация

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