α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
⊢ m₁ ≤ trim m₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
⊢ m₁ ≤ trim m₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
let me := extend (fun s (_p : MeasurableSet s) => measureOf m₂ s)
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
me_empty : me ∅ = 0
⊢ m₁ ≤ trim m₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
⊢ m₁ ≤ trim m₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
have me_empty : me ∅ = 0 := by apply extend_empty; simp; simp
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
me_empty : me ∅ = 0
this : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔ ∀ (s : Set α), ↑m₁ s ≤ me s
⊢ m₁ ≤ trim m₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
me_empty : me ∅ = 0
⊢ m₁ ≤ trim m₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
have : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔
        (∀ (s : Set α), measureOf m₁ s ≤ me s) := le_ofFunction
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
me_empty : me ∅ = 0
this : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔ ∀ (s : Set α), ↑m₁ s ≤ me s
⊢ (∀ (s : Set α), ↑m₁ s ≤ me s) ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
me_empty : me ∅ = 0
this : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔ ∀ (s : Set α), ↑m₁ s ≤ me s
⊢ m₁ ≤ trim m₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
apply this.trans
case h
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
me_empty : me ∅ = 0
this : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔ ∀ (s : Set α), ↑m₁ s ≤ me s
⊢ ∀ (a : Set α), ↑m₁ a ≤ me a ↔ MeasurableSet a → ↑m₁ a ≤ ↑m₂ a
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
me_empty : me ∅ = 0
this : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔ ∀ (s : Set α), ↑m₁ s ≤ me s
⊢ (∀ (s : Set α), ↑m₁ s ≤ me s) ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
apply forall_congr'
case h
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
me_empty : me ∅ = 0
this : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔ ∀ (s : Set α), ↑m₁ s ≤ me s
s : Set α
⊢ ↑m₁ s ≤ me s ↔ MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
case h
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
me_empty : me ∅ = 0
this : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔ ∀ (s : Set α), ↑m₁ s ≤ me s
⊢ ∀ (a : Set α), ↑m₁ a ≤ me a ↔ MeasurableSet a → ↑m₁ a ≤ ↑m₂ a
intro s
no goals
case h
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
me_empty : me ∅ = 0
this : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔ ∀ (s : Set α), ↑m₁ s ≤ me s
s : Set α
⊢ ↑m₁ s ≤ me s ↔ MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
apply le_iInf_iff
case m0
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
⊢ ↑m₂ ∅ = 0

case P0
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
⊢ MeasurableSet ∅
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
⊢ me ∅ = 0
apply extend_empty
case P0
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
⊢ MeasurableSet ∅
case m0
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
⊢ ↑m₂ ∅ = 0

case P0
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
⊢ MeasurableSet ∅
simp
no goals
case P0
α : Type u_1
inst✝ : MeasurableSpace α
m m₁ m₂ : OuterMeasure α
me : Set α → ℝ≥0∞ := extend fun s _p => ↑m₂ s
⊢ MeasurableSet ∅
simp