edist_eq_iSup

Mathlib.Analysis.Normed.Lp.PiLp

URI: https://scilib.ai/kg/mathlib#PiLp.edist_eq_iSup

English

When p = ∞, edist is the supremum over coordinates: edist(f,g) = ⨆ i, edist(f_i,g_i).

Русский

При p = ∞ edist является верхней гранью по координатам: edist(f,g) = ⨆ i, edist(f_i,g_i).

LaTeX

$$$$edist(f,g)=\\big\\lVert (edist(f_i,g_i))_{i}\\big\\rVert_{\\infty}=\\bigsup_i edist(f_i,g_i)$$$$

Lean4

theorem edist_eq_iSup (f g : PiLp ∞ β) : edist f g = ⨆ i, edist (f i) (g i) :=
  rfl

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

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

Разделы

Аффилиация

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