gaugeRescale_self

Mathlib.Analysis.Convex.GaugeRescale

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

← MathLib Explorer

English

The gaugeRescale map with itself as both parameters is the identity map.

Русский

Гейдж-скейл с теми же множителями даёт тождественное отображение.

LaTeX

$$$\\operatorname{gaugeRescale}(s,s) = \\operatorname{id}$$$

Lean4

theorem gaugeRescale_self {s : Set E} (hsa : Absorbent ℝ s) (hsb : IsVonNBounded ℝ s) : gaugeRescale s s = id :=
  funext <| gaugeRescale_self_apply hsa hsb

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

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

Разделы

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

Аффилиация

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