indicatorConstLp_disjoint_union — Mathlib

English

The coeFn of indicatorConstLp equals the corresponding toLp element almost everywhere.

Русский

Сопоставление indicatorConstLp через коэф- функцию совпадает с элементом toLp почти всюду.

LaTeX

$$indicatorConstLp_coeFn = toLp_eq_toLp_iff for appropriate μ.$$

Lean4

/-- The indicator of a disjoint union of two sets is the sum of the indicators of the sets. -/
theorem indicatorConstLp_disjoint_union {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞)
    (hμt : μ t ≠ ∞) (hst : Disjoint s t) (c : E) :
    indicatorConstLp p (hs.union ht) (measure_union_ne_top hμs hμt) c =
      indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c :=
  by
  ext1
  grw [Lp.coeFn_add, indicatorConstLp_coeFn]
  refine EventuallyEq.trans ?_ (EventuallyEq.fun_add indicatorConstLp_coeFn.symm indicatorConstLp_coeFn.symm)
  rw [Set.indicator_union_of_disjoint hst]

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