α : Type u_1
E : Type ?u.328590
F : Type u_2
F' : Type ?u.328596
G : Type ?u.328599
𝕜 : Type ?u.328602
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
G' : Type ?u.328902
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : F), ↑(T s) x ≤ ↑(T' s) x
f : α →ₛ F
⊢ ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) x ≤ ∑ x in SimpleFunc.range f, ↑(T' (↑f ⁻¹' {x})) x
α : Type u_1
E : Type ?u.328590
F : Type u_2
F' : Type ?u.328596
G : Type ?u.328599
𝕜 : Type ?u.328602
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
G' : Type ?u.328902
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : F), ↑(T s) x ≤ ↑(T' s) x
f : α →ₛ F
⊢ setToSimpleFunc T f ≤ setToSimpleFunc T' f
simp_rw [setToSimpleFunc]
no goals
α : Type u_1
E : Type ?u.328590
F : Type u_2
F' : Type ?u.328596
G : Type ?u.328599
𝕜 : Type ?u.328602
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
G' : Type ?u.328902
G'' : Type u_3
inst✝³ : NormedLatticeAddCommGroup G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : NormedLatticeAddCommGroup G'
inst✝ : NormedSpace ℝ G'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : F), ↑(T s) x ≤ ↑(T' s) x
f : α →ₛ F
⊢ ∑ x in SimpleFunc.range f, ↑(T (↑f ⁻¹' {x})) x ≤ ∑ x in SimpleFunc.range f, ↑(T' (↑f ⁻¹' {x})) x
exact sum_le_sum fun i _ => hTT' _ i