G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
this :
  innerContent μ (⨆ (i : ℕ), { carrier := U i, is_open' := (_ : IsOpen (U i)) }) ≤
    ∑' (i : ℕ), innerContent μ { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ innerContent μ { carrier := ⋃ (i : ℕ), U i, is_open' := (_ : IsOpen (⋃ (i : ℕ), U i)) } ≤
    ∑' (i : ℕ), innerContent μ { carrier := U i, is_open' := (_ : IsOpen (U i)) }
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
⊢ innerContent μ { carrier := ⋃ (i : ℕ), U i, is_open' := (_ : IsOpen (⋃ (i : ℕ), U i)) } ≤
    ∑' (i : ℕ), innerContent μ { carrier := U i, is_open' := (_ : IsOpen (U i)) }
have := μ.innerContent_iSup_nat fun i => ⟨U i, hU i⟩
no goals
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
this :
  innerContent μ (⨆ (i : ℕ), { carrier := U i, is_open' := (_ : IsOpen (U i)) }) ≤
    ∑' (i : ℕ), innerContent μ { carrier := U i, is_open' := (_ : IsOpen (U i)) }
⊢ innerContent μ { carrier := ⋃ (i : ℕ), U i, is_open' := (_ : IsOpen (⋃ (i : ℕ), U i)) } ≤
    ∑' (i : ℕ), innerContent μ { carrier := U i, is_open' := (_ : IsOpen (U i)) }
rwa [Opens.iSup_def] at this