ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
⊢ AEMeasurable g
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
⊢ AEMeasurable g
haveI : Nonempty α := ⟨x⟩
case intro
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ AEMeasurable g
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
⊢ AEMeasurable g
obtain ⟨u, hu_tendsto⟩ := exists_seq_tendsto (atTop : Filter α)
case intro
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
⊢ AEMeasurable g
case intro
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ AEMeasurable g
have Ioi_eq_iUnion : Ioi x = ⋃ n : ℕ, Ioc x (u n) := by
  rw [iUnion_Ioc_eq_Ioi_self_iff.mpr _]
  exact fun y _ => (hu_tendsto.eventually (eventually_ge_atTop y)).exists
case intro
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
⊢ ∀ (i : ℕ), AEMeasurable g
case intro
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
⊢ AEMeasurable g
rw [Ioi_eq_iUnion, aemeasurable_iUnion_iff]
case intro
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
⊢ AEMeasurable g
case intro
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
⊢ ∀ (i : ℕ), AEMeasurable g
intro n
case intro.inl
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : x < u n
⊢ AEMeasurable g

case intro.inr
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g
case intro
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
⊢ AEMeasurable g
cases' lt_or_le x (u n) with h h
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ ∀ (x_1 : α), x < x_1 → ∃ i, x_1 ≤ u i
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ Ioi x = ⋃ (n : ℕ), Ioc x (u n)
rw [iUnion_Ioc_eq_Ioi_self_iff.mpr _]
no goals
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ ∀ (x_1 : α), x < x_1 → ∃ i, x_1 ≤ u i
exact fun y _ => (hu_tendsto.eventually (eventually_ge_atTop y)).exists
no goals
case intro.inl
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : x < u n
⊢ AEMeasurable g
exact g_meas (u n) h
case intro.inr
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g
case intro.inr
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g
rw [Ioc_eq_empty (not_lt.mpr h), Measure.restrict_empty]
no goals
case intro.inr
ι : Type ?u.4550285
α : Type u_2
β✝ : Type ?u.4550291
γ : Type ?u.4550294
δ : Type ?u.4550297
R : Type ?u.4550300
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : MeasureTheory.Measure α
β : Type u_1
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g
exact aemeasurable_zero_measure