cthickening_max_zero

Mathlib.Topology.MetricSpace.Thickening

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

← MathLib Explorer

English

cthickening (max 0 δ) E = cthickening δ E for all δ.

Русский

cthickening (max 0 δ) E = cthickening δ E для любых δ.

LaTeX

$$$ cthickening (\max(0, δ)) E = cthickening δ E $$$

Lean4

theorem cthickening_max_zero (δ : ℝ) (E : Set α) : cthickening (max 0 δ) E = cthickening δ E := by
  cases le_total δ 0 <;> simp [cthickening_of_nonpos, *]

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

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

Разделы

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

Аффилиация

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