setToL1_zero_left — Mathlib

English

If T and T' are dominated and equal as sets, then the L1-transforms of f agree, i.e., setToL1 hT f = setToL1 hT' f for all f.

Русский

Если T и T' ограничены и совпадают как множества, то их преобразования L1 совпадают: setToL1 hT f = setToL1 hT' f для всех f.

LaTeX

$$$T=T' \\Rightarrow \\forall f,\\; \\mathrm{setToL1}\\ hT\\ f = \\mathrm{setToL1}\\ hT'\\ f.$$$

Lean4

@[simp]
theorem setToL1_zero_left (hT : DominatedFinMeasAdditive μ (0 : Set α → E →L[ℝ] F) C) (f : α →₁[μ] E) :
    setToL1 hT f = 0 := by
  suffices setToL1 hT = 0 by rw [this]; simp
  refine ContinuousLinearMap.extend_unique (setToL1SCLM α E μ hT) _ _ _ _ ?_
  ext1 f
  rw [setToL1SCLM_zero_left hT f, ContinuousLinearMap.zero_comp, ContinuousLinearMap.zero_apply]

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