toL1_eq_toL1_iff — Mathlib

English

A simplification: equality of toL1 representations implies almost everywhere equality.

Русский

Упрощение: равенство представлений toL1 влечет почти везде равенство.

LaTeX

$$toL1_eq_toL1_iff (f,g) hf hg : toL1 f hf = toL1 g hg ↔ f =ᵐ[μ] g$$

Lean4

@[simp]
theorem toL1_eq_toL1_iff (f g : α → β) (hf : Integrable f μ) (hg : Integrable g μ) :
    toL1 f hf = toL1 g hg ↔ f =ᵐ[μ] g :=
  MemLp.toLp_eq_toLp_iff _ _

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