dist_eq_norm

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.dist_eq_norm

English

The distance between f and g equals the norm of their difference: dist f g = ‖f − g‖.

Русский

Расстояние между f и g равно норме их разности: dist f g = ‖f − g‖.

LaTeX

$$dist(f,g) = \|f - g\|$$

Lean4

theorem dist_eq_norm (f g : Lp E p μ) : dist f g = ‖f - g‖ :=
  rfl

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

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

Разделы

Аффилиация

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