α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
rw [OuterMeasure.sInf_eq_boundedBy_sInfGen]
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
⊢ OuterMeasure.sInfGen (toOuterMeasure '' m) (t ∩ s) + OuterMeasure.sInfGen (toOuterMeasure '' m) (t \ s) ≤
    OuterMeasure.sInfGen (toOuterMeasure '' m) t
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
refine' OuterMeasure.boundedBy_caratheodory fun t => _
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ∀ (x : Measure α),
    x ∈ m →
      ∀ (i : Set α),
        t ⊆ i →
          MeasurableSet i →
            ((⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t ∩ s)) +
                ⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t \ s)) ≤
              ↑↑x i
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
⊢ OuterMeasure.sInfGen (toOuterMeasure '' m) (t ∩ s) + OuterMeasure.sInfGen (toOuterMeasure '' m) (t \ s) ≤
    OuterMeasure.sInfGen (toOuterMeasure '' m) t
simp only [OuterMeasure.sInfGen, le_iInf_iff, ball_image_iff,
  measure_eq_iInf t]
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
⊢ ((⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t ∩ s)) +
      ⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t \ s)) ≤
    ↑↑μ u
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ∀ (x : Measure α),
    x ∈ m →
      ∀ (i : Set α),
        t ⊆ i →
          MeasurableSet i →
            ((⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t ∩ s)) +
                ⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t \ s)) ≤
              ↑↑x i
intro μ hμ u htu _hu
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ ↑↑μ t
⊢ ((⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t ∩ s)) +
      ⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t \ s)) ≤
    ↑↑μ u
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
⊢ ((⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t ∩ s)) +
      ⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t \ s)) ≤
    ↑↑μ u
have hm : ∀ {s t}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t := by
  intro s t hst
  rw [OuterMeasure.sInfGen_def]
  refine' iInf_le_of_le μ.toOuterMeasure (iInf_le_of_le (mem_image_of_mem _ hμ) _)
  refine' measure_mono hst
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ ↑↑μ t
⊢ ((⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t ∩ s)) +
      ⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t \ s)) ≤
    ↑↑μ (u ∩ s) + ↑↑μ (u \ s)
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ ↑↑μ t
⊢ ((⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t ∩ s)) +
      ⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t \ s)) ≤
    ↑↑μ u
rw [← measure_inter_add_diff u hs]
no goals
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ ↑↑μ t
⊢ ((⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t ∩ s)) +
      ⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ (t \ s)) ≤
    ↑↑μ (u ∩ s) + ↑↑μ (u \ s)
refine' add_le_add (hm <| inter_subset_inter_left _ htu) (hm <| diff_subset_diff_left htu)
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝¹ s' t✝¹ : Set α
m : Set (Measure α)
s✝ : Set α
hs : MeasurableSet s✝
t✝ : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t✝ ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ ↑↑μ t
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
⊢ ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ ↑↑μ t
intro s t hst
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝¹ s' t✝¹ : Set α
m : Set (Measure α)
s✝ : Set α
hs : MeasurableSet s✝
t✝ : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t✝ ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ (⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ s) ≤ ↑↑μ t
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝¹ s' t✝¹ : Set α
m : Set (Measure α)
s✝ : Set α
hs : MeasurableSet s✝
t✝ : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t✝ ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ ↑↑μ t
rw [OuterMeasure.sInfGen_def]
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝¹ s' t✝¹ : Set α
m : Set (Measure α)
s✝ : Set α
hs : MeasurableSet s✝
t✝ : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t✝ ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ ↑↑μ s ≤ ↑↑μ t
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝¹ s' t✝¹ : Set α
m : Set (Measure α)
s✝ : Set α
hs : MeasurableSet s✝
t✝ : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t✝ ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ (⨅ (μ : OuterMeasure α) (_ : μ ∈ toOuterMeasure '' m), ↑μ s) ≤ ↑↑μ t
refine' iInf_le_of_le μ.toOuterMeasure (iInf_le_of_le (mem_image_of_mem _ hμ) _)
no goals
α : Type u_1
β : Type ?u.147381
γ : Type ?u.147384
δ : Type ?u.147387
ι : Type ?u.147390
R : Type ?u.147393
R' : Type ?u.147396
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝¹ s' t✝¹ : Set α
m : Set (Measure α)
s✝ : Set α
hs : MeasurableSet s✝
t✝ : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t✝ ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ ↑↑μ s ≤ ↑↑μ t
refine' measure_mono hst