toLp_congr

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.MemLp.toLp_congr

English

For MemLp f p μ and MemLp g p μ, hf.toLp f equals hg.toLp g if and only if f and g are equal almost everywhere with respect to μ.

Русский

Для MemLp f p μ и MemLp g p μ, hf.toLp f = hg.toLp g тогда и только тогда, когда f =ᵐ μ g.

LaTeX

$$hf.toLp f = hg.toLp g ↔ f =ᵐ[μ] g$$

Lean4

theorem toLp_congr {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) (hfg : f =ᵐ[μ] g) : hf.toLp f = hg.toLp g := by
  simp [toLp, hfg]

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

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

Разделы

Аффилиация

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