α : Type u_1
E : Type ?u.29157
F : Type ?u.29160
F' : Type ?u.29163
G : Type ?u.29166
𝕜 : Type ?u.29169
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✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑μ s = ⊤
⊢ ↑↑(c • μ) s = ⊤
α : Type u_1
E : Type ?u.29157
F : Type ?u.29160
F' : Type ?u.29163
G : Type ?u.29166
𝕜 : Type ?u.29169
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✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
⊢ FinMeasAdditive (c • μ) T
refine' of_eq_top_imp_eq_top (fun s _ hμs => _) hT
α : Type u_1
E : Type ?u.29157
F : Type ?u.29160
F' : Type ?u.29163
G : Type ?u.29166
𝕜 : Type ?u.29169
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✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑μ s = ⊤
⊢ c ≠ 0 ∧ ↑↑μ s = ⊤ ∨ c = ⊤ ∧ ↑↑μ s ≠ 0
α : Type u_1
E : Type ?u.29157
F : Type ?u.29160
F' : Type ?u.29163
G : Type ?u.29166
𝕜 : Type ?u.29169
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✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑μ s = ⊤
⊢ ↑↑(c • μ) s = ⊤
rw [Measure.smul_apply, smul_eq_mul, ENNReal.mul_eq_top]
α : Type u_1
E : Type ?u.29157
F : Type ?u.29160
F' : Type ?u.29163
G : Type ?u.29166
𝕜 : Type ?u.29169
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✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑μ s = ⊤
⊢ ↑↑μ s = ⊤ ∨ c = ⊤ ∧ ¬↑↑μ s = 0
α : Type u_1
E : Type ?u.29157
F : Type ?u.29160
F' : Type ?u.29163
G : Type ?u.29166
𝕜 : Type ?u.29169
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✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑μ s = ⊤
⊢ c ≠ 0 ∧ ↑↑μ s = ⊤ ∨ c = ⊤ ∧ ↑↑μ s ≠ 0
simp only [hc_ne_zero, true_and_iff, Ne.def, not_false_iff]
no goals
α : Type u_1
E : Type ?u.29157
F : Type ?u.29160
F' : Type ?u.29163
G : Type ?u.29166
𝕜 : Type ?u.29169
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✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_zero : c ≠ 0
hT : FinMeasAdditive μ T
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑μ s = ⊤
⊢ ↑↑μ s = ⊤ ∨ c = ⊤ ∧ ¬↑↑μ s = 0
exact Or.inl hμs