setToSimpleFunc_nonneg — Mathlib

English

If T and T' satisfy a pointwise order T s x ≤ T' s x for all s and x, then setToSimpleFunc T f ≤ setToSimpleFunc T' f for any simple function f.

Русский

Если для всех s и x выполняется неравенство T s x ≤ T' s x, то для любой простой функции f имеет место неравенство setToSimpleFunc T f ≤ setToSimpleFunc T' f.

LaTeX

$$$\forall s x,\; T s x \le T' s x \Rightarrow setToSimpleFunc T f \le setToSimpleFunc T' f $$$

Lean4

theorem setToSimpleFunc_nonneg {m : MeasurableSpace α} (T : Set α → G' →L[ℝ] G'') (hT_nonneg : ∀ s x, 0 ≤ x → 0 ≤ T s x)
    (f : α →ₛ G') (hf : 0 ≤ f) : 0 ≤ setToSimpleFunc T f :=
  by
  refine sum_nonneg fun i hi => hT_nonneg _ i ?_
  rw [mem_range] at hi
  obtain ⟨y, hy⟩ := Set.mem_range.mp hi
  rw [← hy]
  refine le_trans ?_ (hf y)
  simp

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