edist_smul_Lp

Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic

URI: https://scilib.ai/kg/mathlib#DomMulAct.edist_smul_Lp

← MathLib Explorer

English

The edist is preserved under DomMulAct smul: edist (c•f) (c•g) = edist f g.

Русский

Edist сохраняется под умножением DomMulAct: edist(c•f, c•g) = edist(f,g).

LaTeX

$$edist (c • f) (c • g) = edist f g$$

Lean4

@[to_additive (attr := simp)]
theorem edist_smul_Lp (c : Mᵈᵐᵃ) (f g : Lp E p μ) : edist (c • f) (c • g) = edist f g := by
  simp only [Lp.edist_dist, dist_smul_Lp]

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

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

Разделы

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

Аффилиация

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