dist_edist

Mathlib.MeasureTheory.Function.LpSpace.Basic

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

English

The distance equals the real of edistance: dist f g = (edist f g).toReal.

Русский

Расстояние равно действительному значению edist: dist f g = (edist f g).toReal.

LaTeX

$$dist(f,g) = (edist(f,g)).toReal$$

Lean4

protected theorem dist_edist (f g : Lp E p μ) : dist f g = (edist f g).toReal :=
  MeasureTheory.Lp.dist_def ..

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

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

Разделы

Аффилиация

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