smul — Mathlib

English

A variant statement asserting μ(s) < ∞ for a measurable set s when a certain indicator-like function lies in MemLp.

Русский

Вариант утверждения о мере множества s при условии, что индикатороподобная функция принадлежит MemLp.

LaTeX

$$$\\mathrm{measure\\_lt\\_top\\_of\\_memLp\\_indicator\\_simp}$$$

Lean4

/-- If `E` is a normed space, `Lp.simpleFunc E p μ` is a `SMul`. Not declared as an
instance as it is (as of writing) used only in the construction of the Bochner integral. -/
protected def smul : SMul 𝕜 (Lp.simpleFunc E p μ) :=
  ⟨fun k f =>
    ⟨k • (f : Lp E p μ), by
      rcases f with ⟨f, ⟨s, hs⟩⟩
      use k • s
      apply Eq.trans (AEEqFun.smul_mk k s s.aestronglyMeasurable).symm _
      rw [hs]
      rfl⟩⟩

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