α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ (AEMeasurable f ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t) → AEStronglyMeasurable f μ
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ AEStronglyMeasurable f μ ↔ AEMeasurable f ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
refine' ⟨fun H => ⟨H.aemeasurable, H.isSeparable_ae_range⟩, _⟩
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEStronglyMeasurable f μ
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ (AEMeasurable f ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t) → AEStronglyMeasurable f μ
rintro ⟨H, ⟨t, t_sep, ht⟩⟩
case intro.intro.intro.inl
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t_sep : IsSeparable ∅
ht : ∀ᵐ (x : α) ∂μ, f x ∈ ∅
⊢ AEStronglyMeasurable f μ

case intro.intro.intro.inr
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
⊢ AEStronglyMeasurable f μ
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEStronglyMeasurable f μ
rcases eq_empty_or_nonempty t with (rfl | h₀)
case intro.intro.intro.inl
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t_sep : IsSeparable ∅
ht : μ = 0
⊢ AEStronglyMeasurable f μ
case intro.intro.intro.inl
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t_sep : IsSeparable ∅
ht : ∀ᵐ (x : α) ∂μ, f x ∈ ∅
⊢ AEStronglyMeasurable f μ
simp only [mem_empty_iff_false, eventually_false_iff_eq_bot, ae_eq_bot] at ht
case intro.intro.intro.inl
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t_sep : IsSeparable ∅
ht : μ = 0
⊢ AEStronglyMeasurable f 0
case intro.intro.intro.inl
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t_sep : IsSeparable ∅
ht : μ = 0
⊢ AEStronglyMeasurable f μ
rw [ht]
no goals
case intro.intro.intro.inl
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t_sep : IsSeparable ∅
ht : μ = 0
⊢ AEStronglyMeasurable f 0
exact aestronglyMeasurable_zero_measure f
case intro.intro.intro.inr.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g✝ : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
g : α → β
g_meas : Measurable g
gt : range g ⊆ t
fg : f =ᶠ[ae μ] g
⊢ AEStronglyMeasurable f μ
case intro.intro.intro.inr
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
⊢ AEStronglyMeasurable f μ
obtain ⟨g, g_meas, gt, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g :=
  H.exists_ae_eq_range_subset ht h₀
case intro.intro.intro.inr.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g✝ : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
g : α → β
g_meas : Measurable g
gt : range g ⊆ t
fg : f =ᶠ[ae μ] g
⊢ StronglyMeasurable g
case intro.intro.intro.inr.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g✝ : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
g : α → β
g_meas : Measurable g
gt : range g ⊆ t
fg : f =ᶠ[ae μ] g
⊢ AEStronglyMeasurable f μ
refine' ⟨g, _, fg⟩
no goals
case intro.intro.intro.inr.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.349684
ι : Type ?u.349687
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g✝ : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
g : α → β
g_meas : Measurable g
gt : range g ⊆ t
fg : f =ᶠ[ae μ] g
⊢ StronglyMeasurable g
exact stronglyMeasurable_iff_measurable_separable.2 ⟨g_meas, t_sep.mono gt⟩