gauge_neg_set_eq_gauge_neg

Mathlib.Analysis.Convex.Gauge

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

English

Equality gauge(-s,x) = gauge(s,−x).

Русский

Равенство gauge(-s,x) = gauge(s,−x).

LaTeX

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

Lean4

theorem gauge_neg_set_eq_gauge_neg (x : E) : gauge (-s) x = gauge s (-x) := by rw [← gauge_neg_set_neg, neg_neg]

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

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

Разделы

Аффилиация

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