G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ MeasurableSet A ↔
    ∀ (U : Set G) (hU : IsOpen U),
      ↑(Content.outerMeasure μ) (↑{ carrier := U, is_open' := hU } ∩ A) +
          ↑(Content.outerMeasure μ) (↑{ carrier := U, is_open' := hU } \ A) ≤
        ↑(Content.outerMeasure μ) ↑{ carrier := U, is_open' := hU }
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ MeasurableSet A ↔
    ∀ (U : Opens G),
      ↑(Content.outerMeasure μ) (↑U ∩ A) + ↑(Content.outerMeasure μ) (↑U \ A) ≤ ↑(Content.outerMeasure μ) ↑U
rw [Opens.forall]
case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    innerContent μ { carrier := ⋃ (i : ℕ), f i, is_open' := (_ : ?P (⋃ (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
A : Set 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₂ }

case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ (i : ℕ), f i)
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ MeasurableSet A ↔
    ∀ (U : Set G) (hU : IsOpen U),
      ↑(Content.outerMeasure μ) (↑{ carrier := U, is_open' := hU } ∩ A) +
          ↑(Content.outerMeasure μ) (↑{ carrier := U, is_open' := hU } \ A) ≤
        ↑(Content.outerMeasure μ) ↑{ carrier := U, is_open' := hU }
apply inducedOuterMeasure_caratheodory
case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set 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₂ }
case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    innerContent μ { carrier := ⋃ (i : ℕ), f i, is_open' := (_ : ?P (⋃ (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
A : Set 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₂ }

case PU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set G
⊢ ∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ (i : ℕ), f i)
apply innerContent_iUnion_nat
no goals
case m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : T2Space G
A : Set 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₂ }
apply innerContent_mono'