dist_eq_iSup

Mathlib.Analysis.Normed.Lp.PiLp

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

English

For p=∞, dist equals the iSup of coordinate distances: dist f g = ⨆ i, dist(f_i,g_i).

Русский

Для p=∞ расстояние равно sup по координатам: dist f g = ⨆ i, dist(f_i,g_i).

LaTeX

$$$$dist(f,g)=\\bigsup_i dist(f_i,g_i)$$$$

Lean4

theorem dist_eq_iSup (f g : PiLp ∞ α) : dist f g = ⨆ i, dist (f i) (g i) :=
  rfl

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

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

Разделы

Аффилиация

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