gauge_of_subset_zero

Mathlib.Analysis.Convex.Gauge

URI: https://scilib.ai/kg/mathlib#gauge_of_subset_zero

English

If s is contained in {0}, gauge s = 0 (alternative).

Русский

Если s ⊆ {0}, gauge s = 0 (альтернативно).

LaTeX

$$$$ s \\subseteq \\{0\\} \\implies \\operatorname{gauge}(s) = 0. $$$$

Lean4

theorem gauge_of_subset_zero (h : s ⊆ 0) : gauge s = 0 :=
  by
  obtain rfl | rfl := subset_singleton_iff_eq.1 h
  exacts [gauge_empty, gauge_zero']

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

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

Разделы

Аффилиация

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