ae_eq

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

English

If f =ᵐ[μ] g and g ∈ MemLp p μ, then f ∈ MemLp p μ.

Русский

Если f =ᵐ g и g ∈ MemLp, то f ∈ MemLp.

LaTeX

$$$(f=\!\!a_e g)\Rightarrow (MemLp g p μ) \Rightarrow MemLp f p μ.$$$

Lean4

theorem ae_eq [TopologicalSpace ε] {f g : α → ε} (hfg : f =ᵐ[μ] g) (hf_Lp : MemLp f p μ) : MemLp g p μ :=
  (memLp_congr_ae hfg).1 hf_Lp

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

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

Разделы

Аффилиация

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