toL1_eq_mk — Mathlib

English

Given integrable f and g, equality of their L1 representations is equivalent to almost everywhere equality of f and g.

Русский

Для интегрируемых f и g равенство их представлений в toL1 эквивалентно почти везде равенству f и g.

LaTeX

$$toL1 f hf = toL1 g hg \iff f =ᵐ[μ] g$$

Lean4

@[simp]
theorem toL1_eq_mk (f : α → β) (hf : Integrable f μ) : (hf.toL1 f : α →ₘ[μ] β) = AEEqFun.mk f hf.aestronglyMeasurable :=
  rfl

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