α : Type u_1
E : Type ?u.97713
F : Type ?u.97716
F' : Type ?u.97719
G : Type ?u.97722
𝕜 : Type ?u.97725
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_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s < ⊤
⊢ ‖OfNat.ofNat 0 s‖ ≤ C * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type ?u.97713
F : Type ?u.97716
F' : Type ?u.97719
G : Type ?u.97722
𝕜 : Type ?u.97725
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_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive μ 0 C
refine' ⟨FinMeasAdditive.zero, fun s _ _ => _⟩
α : Type u_1
E : Type ?u.97713
F : Type ?u.97716
F' : Type ?u.97719
G : Type ?u.97722
𝕜 : Type ?u.97725
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_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s < ⊤
⊢ 0 ≤ C * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type ?u.97713
F : Type ?u.97716
F' : Type ?u.97719
G : Type ?u.97722
𝕜 : Type ?u.97725
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_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s < ⊤
⊢ ‖OfNat.ofNat 0 s‖ ≤ C * ENNReal.toReal (↑↑μ s)
rw [Pi.zero_apply, norm_zero]
no goals
α : Type u_1
E : Type ?u.97713
F : Type ?u.97716
F' : Type ?u.97719
G : Type ?u.97722
𝕜 : Type ?u.97725
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_2
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
m : MeasurableSpace α
μ : Measure α
hC : 0 ≤ C
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s < ⊤
⊢ 0 ≤ C * ENNReal.toReal (↑↑μ s)
exact mul_nonneg hC toReal_nonneg