simpleFunc — Mathlib

English

A variant of the previous indicator result under a simpler formulation.

Русский

Вариант предыдущего результата для индикатора в более простой форме.

LaTeX

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

Lean4

/-- `Lp.simpleFunc` is a subspace of Lp consisting of equivalence classes of an integrable simple
function. -/
def simpleFunc : AddSubgroup (Lp E p μ)
    where
  carrier := {f : Lp E p μ | ∃ s : α →ₛ E, (AEEqFun.mk s s.aestronglyMeasurable : α →ₘ[μ] E) = f}
  zero_mem' := ⟨0, rfl⟩
  add_mem' := by
    rintro f g ⟨s, hs⟩ ⟨t, ht⟩
    use s + t
    simp only [← hs, ← ht, AEEqFun.mk_add_mk, AddSubgroup.coe_add, SimpleFunc.coe_add]
  neg_mem' := by
    rintro f ⟨s, hs⟩
    use -s
    simp only [← hs, AEEqFun.neg_mk, SimpleFunc.coe_neg, AddSubgroup.coe_neg]

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