G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤
    ⨅ (t : Set G) (ht : IsOpen t) (_ : ↑K ⊆ t), innerContent μ { carrier := t, is_open' := ht }

case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ (i : ℕ), f i)

case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    innerContent μ { carrier := ⋃ (i : ℕ), f i, is_open' := (_ : ?m.41098 (⋃ (i : ℕ), f i)) } ≤
      ∑' (i : ℕ), innerContent μ { carrier := f i, is_open' := (_ : IsOpen (f i)) }

case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → innerContent μ { carrier := s₁, is_open' := hs₁ } ≤ innerContent μ { carrier := s₂, is_open' := hs₂ }
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤ ↑(Content.outerMeasure μ) ↑K
rw [Content.outerMeasure, inducedOuterMeasure_eq_iInf]
no goals
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤
    ⨅ (t : Set G) (ht : IsOpen t) (_ : ↑K ⊆ t), innerContent μ { carrier := t, is_open' := ht }
exact le_iInf fun U => le_iInf fun hU => le_iInf <| μ.le_innerContent K ⟨U, hU⟩
no goals
case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ (i : ℕ), f i)
exact fun U hU => isOpen_iUnion hU
no goals
case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    innerContent μ { carrier := ⋃ (i : ℕ), f i, is_open' := (_ : IsOpen (⋃ (i : ℕ), (fun i => f i) i)) } ≤
      ∑' (i : ℕ), innerContent μ { carrier := f i, is_open' := (_ : IsOpen (f i)) }
exact μ.innerContent_iUnion_nat
no goals
case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
K : Compacts G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → innerContent μ { carrier := s₁, is_open' := hs₁ } ≤ innerContent μ { carrier := s₂, is_open' := hs₂ }
exact μ.innerContent_mono