gauge_neg_set_neg

Mathlib.Analysis.Convex.Gauge

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

English

Gauge symmetry under negation holds for general negation operator.

Русский

Обобщённая симметрия gauge при отрицании сохраняется.

LaTeX

$$$$\\operatorname{gauge}((-s), (-x)) = \\operatorname{gauge}(s, x).$$$$

Lean4

theorem gauge_neg_set_neg (x : E) : gauge (-s) (-x) = gauge s x := by simp_rw [gauge_def', smul_neg, neg_mem_neg]

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

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

Разделы

Аффилиация

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