ext

Mathlib.MeasureTheory.Function.LpSpace.Basic

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

English

If two Lp representatives f and g are almost everywhere equal, then they are equal in Lp.

Русский

Если две функции-представителя Lp равны почти везде, то они равны в Lp.

LaTeX

$$f =ᵐ[μ] g → f = g (in Lp E p μ)$$

Lean4

@[ext high]
theorem ext {f g : Lp E p μ} (h : f =ᵐ[μ] g) : f = g := by
  cases f
  cases g
  simp only [Subtype.mk_eq_mk]
  exact AEEqFun.ext h

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

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

Разделы

Аффилиация

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