English
An element f ∈ Lp(E,p,μ) belongs to the subgroup of Lp consisting of classes containing a bounded continuous representative if and only if there exists f0: α→ᵇE with f0.toContinuousMap.toAEEqFun μ = f as an Lp class.
Русский
Элемент f ∈ Lp(E,p,μ) принадлежит подгруппе, содержащей ограниченного непрерывного представителя, тогда и только тогда существует f0: α→ᵇE, для которого эквивалентность по Lp совпадает с f.
LaTeX
$$$f \\in \\mathrm{Lp}_{\\text{bounded}}(E,p,μ) \\iff \\exists f_0:\\alpha\\to\\!^b E,\\; f_0^{\\mathrm{toContinuousMap}}^{toAEEqFun}(μ)=f.$$$
Lean4
/-- By definition, the elements of `Lp.boundedContinuousFunction E p μ` are the elements of
`Lp E p μ` which contain a bounded continuous representative. -/
theorem mem_boundedContinuousFunction_iff {f : Lp E p μ} :
f ∈ MeasureTheory.Lp.boundedContinuousFunction E p μ ↔
∃ f₀ : α →ᵇ E, f₀.toContinuousMap.toAEEqFun μ = (f : α →ₘ[μ] E) :=
AddSubgroup.mem_addSubgroupOf
