no goals
α : Type ?u.159032
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ (c • m) ∅ = 0
simp [m_empty]
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
⊢ ↑(c • OuterMeasure.ofFunction m m_empty) s = ↑(OuterMeasure.ofFunction (c • m) (_ : c • m ∅ = 0)) s
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ c • OuterMeasure.ofFunction m m_empty = OuterMeasure.ofFunction (c • m) (_ : c • m ∅ = 0)
ext1 s
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
this : Nonempty { t // s ⊆ ⋃ (i : ℕ), t i }
⊢ ↑(c • OuterMeasure.ofFunction m m_empty) s = ↑(OuterMeasure.ofFunction (c • m) (_ : c • m ∅ = 0)) s
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
⊢ ↑(c • OuterMeasure.ofFunction m m_empty) s = ↑(OuterMeasure.ofFunction (c • m) (_ : c • m ∅ = 0)) s
haveI : Nonempty { t : ℕ → Set α // s ⊆ ⋃ i, t i } := ⟨⟨fun _ => s, subset_iUnion (fun _ => s) 0⟩⟩
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
this : Nonempty { t // s ⊆ ⋃ (i : ℕ), t i }
⊢ (c * ⨅ (x : { i // s ⊆ iUnion i }), ∑' (n : ℕ), m (↑x n)) = ⨅ (x : { i // s ⊆ iUnion i }), c * ∑' (i : ℕ), m (↑x i)
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
this : Nonempty { t // s ⊆ ⋃ (i : ℕ), t i }
⊢ ↑(c • OuterMeasure.ofFunction m m_empty) s = ↑(OuterMeasure.ofFunction (c • m) (_ : c • m ∅ = 0)) s
simp only [smul_apply, ofFunction_apply, ENNReal.tsum_mul_left, Pi.smul_apply, smul_eq_mul,
iInf_subtype']
no goals
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
this : Nonempty { t // s ⊆ ⋃ (i : ℕ), t i }
⊢ (c * ⨅ (x : { i // s ⊆ iUnion i }), ∑' (n : ℕ), m (↑x n)) = ⨅ (x : { i // s ⊆ iUnion i }), c * ∑' (i : ℕ), m (↑x i)
rw [ENNReal.iInf_mul_left fun h => (hc h).elim]