continuousOn_smul — Mathlib

English

If f ∈ Lp on A and g is ContinuousOn on K with A ⊆ K, then f·g ∈ Lp on A.

Русский

Если f ∈ Lp на A и g непрерывна на K с A ⊆ K, то f·g ∈ Lp на A.

LaTeX

$$$f\cdot g \in L^{p}(A,\mu)$$$

Lean4

theorem continuousOn_smul [T2Space X] [SecondCountableTopologyEither X 𝕜] {g : X → E} (hg : IntegrableOn g K μ)
    {f : X → 𝕜} (hf : ContinuousOn f K) (hK : IsCompact K) : IntegrableOn (fun x => f x • g x) K μ :=
  hg.continuousOn_smul_of_subset hf hK hK.measurableSet Subset.rfl

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