α : Type u_1
β : Type ?u.825109
γ : Type ?u.825112
δ : Type ?u.825115
ι : Type ?u.825118
R : Type ?u.825121
R' : Type ?u.825124
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂Measure.restrict μ s, P x
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
⊢ ∀ᵐ (x : α) ∂μ, P x
α : Type u_1
β : Type ?u.825109
γ : Type ?u.825112
δ : Type ?u.825115
ι : Type ?u.825118
R : Type ?u.825121
R' : Type ?u.825124
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂Measure.restrict μ s, P x
⊢ ∀ᵐ (x : α) ∂μ, P x
have : ∀ n, ∀ᵐ x ∂μ, x ∈ spanningSets (μ + ν) n → P x := by
  intro n
  have := h
    (spanningSets (μ + ν) n) (measurable_spanningSets _ _)
    ((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
    ((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
  exact (ae_restrict_iff' (measurable_spanningSets _ _)).mp this
no goals
α : Type u_1
β : Type ?u.825109
γ : Type ?u.825112
δ : Type ?u.825115
ι : Type ?u.825118
R : Type ?u.825121
R' : Type ?u.825124
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂Measure.restrict μ s, P x
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
⊢ ∀ᵐ (x : α) ∂μ, P x
filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)
α : Type u_1
β : Type ?u.825109
γ : Type ?u.825112
δ : Type ?u.825115
ι : Type ?u.825118
R : Type ?u.825121
R' : Type ?u.825124
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂Measure.restrict μ s, P x
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
α : Type u_1
β : Type ?u.825109
γ : Type ?u.825112
δ : Type ?u.825115
ι : Type ?u.825118
R : Type ?u.825121
R' : Type ?u.825124
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂Measure.restrict μ s, P x
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
intro n
α : Type u_1
β : Type ?u.825109
γ : Type ?u.825112
δ : Type ?u.825115
ι : Type ?u.825118
R : Type ?u.825121
R' : Type ?u.825124
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂Measure.restrict μ s, P x
n : ℕ
this : ∀ᵐ (x : α) ∂Measure.restrict μ (spanningSets (μ + ν) n), P x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
α : Type u_1
β : Type ?u.825109
γ : Type ?u.825112
δ : Type ?u.825115
ι : Type ?u.825118
R : Type ?u.825121
R' : Type ?u.825124
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂Measure.restrict μ s, P x
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
have := h
  (spanningSets (μ + ν) n) (measurable_spanningSets _ _)
  ((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
  ((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
no goals
α : Type u_1
β : Type ?u.825109
γ : Type ?u.825112
δ : Type ?u.825115
ι : Type ?u.825118
R : Type ?u.825121
R' : Type ?u.825124
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂Measure.restrict μ s, P x
n : ℕ
this : ∀ᵐ (x : α) ∂Measure.restrict μ (spanningSets (μ + ν) n), P x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
exact (ae_restrict_iff' (measurable_spanningSets _ _)).mp this