α : Type u_2
E : Type ?u.100491
F : Type ?u.100494
F' : Type ?u.100497
G : Type ?u.100500
𝕜 : Type ?u.100503
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 α
β✝ : Type ?u.100803
inst✝¹ : SeminormedAddCommGroup β✝
T✝ T' : Set α → β✝
C✝ C' : ℝ
β : Type u_1
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : ↑↑μ s = 0
⊢ ‖T s‖ = 0
α : Type u_2
E : Type ?u.100491
F : Type ?u.100494
F' : Type ?u.100497
G : Type ?u.100500
𝕜 : Type ?u.100503
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 α
β✝ : Type ?u.100803
inst✝¹ : SeminormedAddCommGroup β✝
T✝ T' : Set α → β✝
C✝ C' : ℝ
β : Type u_1
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : ↑↑μ s = 0
⊢ T s = 0
refine' norm_eq_zero.mp _
α : Type u_2
E : Type ?u.100491
F : Type ?u.100494
F' : Type ?u.100497
G : Type ?u.100500
𝕜 : Type ?u.100503
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 α
β✝ : Type ?u.100803
inst✝¹ : SeminormedAddCommGroup β✝
T✝ T' : Set α → β✝
C✝ C' : ℝ
β : Type u_1
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : ↑↑μ s = 0
⊢ C * ENNReal.toReal (↑↑μ s) = 0
α : Type u_2
E : Type ?u.100491
F : Type ?u.100494
F' : Type ?u.100497
G : Type ?u.100500
𝕜 : Type ?u.100503
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 α
β✝ : Type ?u.100803
inst✝¹ : SeminormedAddCommGroup β✝
T✝ T' : Set α → β✝
C✝ C' : ℝ
β : Type u_1
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : ↑↑μ s = 0
⊢ ‖T s‖ = 0
refine' ((hT.2 s hs (by simp [hs_zero])).trans (le_of_eq _)).antisymm (norm_nonneg _)
no goals
α : Type u_2
E : Type ?u.100491
F : Type ?u.100494
F' : Type ?u.100497
G : Type ?u.100500
𝕜 : Type ?u.100503
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 α
β✝ : Type ?u.100803
inst✝¹ : SeminormedAddCommGroup β✝
T✝ T' : Set α → β✝
C✝ C' : ℝ
β : Type u_1
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : ↑↑μ s = 0
⊢ C * ENNReal.toReal (↑↑μ s) = 0
rw [hs_zero, ENNReal.zero_toReal, MulZeroClass.mul_zero]
no goals
α : Type u_2
E : Type ?u.100491
F : Type ?u.100494
F' : Type ?u.100497
G : Type ?u.100500
𝕜 : Type ?u.100503
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 α
β✝ : Type ?u.100803
inst✝¹ : SeminormedAddCommGroup β✝
T✝ T' : Set α → β✝
C✝ C' : ℝ
β : Type u_1
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : ↑↑μ s = 0
⊢ ↑↑μ s < ⊤
simp [hs_zero]