setToSimpleFunc_congr_left — Mathlib

English

If T and T' agree on all measurable s (finite μ(s)), then f.setToSimpleFunc T = f.setToSimpleFunc T' for all integrable f.

Русский

Если T и T' совпадают на всех измеримых s с конечной μ(m) — тогда для всех интегрируемых f выполняется равенство f.setToSimpleFunc T = f.setToSimpleFunc T'.

LaTeX

$$$\forall s, MeasurableSet s,\; μ s < ∞ \Rightarrow T s = T' s \Rightarrow \forall f, Integrable f μ \Rightarrow f.setToSimpleFunc T = f.setToSimpleFunc T'$$$

Lean4

theorem setToSimpleFunc_congr_left (T T' : Set α → E →L[ℝ] F) (h : ∀ s, MeasurableSet s → μ s < ∞ → T s = T' s)
    (f : α →ₛ E) (hf : Integrable f μ) : setToSimpleFunc T f = setToSimpleFunc T' f :=
  by
  simp_rw [setToSimpleFunc]
  refine sum_congr rfl fun x _ => ?_
  by_cases hx0 : x = 0
  · simp [hx0]
  ·
    rw [h (f ⁻¹' { x }) (SimpleFunc.measurableSet_fiber _ _)
        (SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hx0)]

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