α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
⊢ ∀ (i : (fun s => MeasurableSet s) s₂), extend m s₁ ≤ m s₂ i
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
⊢ extend m s₁ ≤ extend m s₂
refine' le_iInf _
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : (fun s => MeasurableSet s) s₂
⊢ extend m s₁ ≤ m s₂ h₂
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
⊢ ∀ (i : (fun s => MeasurableSet s) s₂), extend m s₁ ≤ m s₂ i
intro h₂
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : (fun s => MeasurableSet s) s₂
this : extend m (s₁ ∪ s₂ \ s₁) = extend m s₁ + extend m (s₂ \ s₁)
⊢ extend m s₁ ≤ m s₂ h₂
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : (fun s => MeasurableSet s) s₂
⊢ extend m s₁ ≤ m s₂ h₂
have :=
  extend_union MeasurableSet.empty m0 MeasurableSet.iUnion mU disjoint_sdiff_self_right h₁
    (h₂.diff h₁)
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : (fun s => MeasurableSet s) s₂
this : extend m s₂ = extend m s₁ + extend m (s₂ \ s₁)
⊢ extend m s₁ ≤ m s₂ h₂
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : (fun s => MeasurableSet s) s₂
this : extend m (s₁ ∪ s₂ \ s₁) = extend m s₁ + extend m (s₂ \ s₁)
⊢ extend m s₁ ≤ m s₂ h₂
rw [union_diff_cancel hs] at this
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : (fun s => MeasurableSet s) s₂
this : extend m s₂ = extend m s₁ + extend m (s₂ \ s₁)
⊢ extend m s₁ ≤ extend m s₂
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : (fun s => MeasurableSet s) s₂
this : extend m s₂ = extend m s₁ + extend m (s₂ \ s₁)
⊢ extend m s₁ ≤ m s₂ h₂
rw [← extend_eq m]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ (_ : MeasurableSet ∅) = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      m (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) = ∑' (i : ℕ), m (f i) (_ : MeasurableSet (f i))
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : (fun s => MeasurableSet s) s₂
this : extend m s₂ = extend m s₁ + extend m (s₂ \ s₁)
⊢ extend m s₁ ≤ extend m s₂
exact le_iff_exists_add.2 ⟨_, this⟩