α : Type u_2
β : Type u_3
γ✝ : Type ?u.350679
ι : Type ?u.350682
inst✝² : Countable ι
m : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ✝
f✝ g✝ : α → β
γ : Type u_1
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
⊢ AEStronglyMeasurable (g ∘ f) μ → AEStronglyMeasurable g (Measure.map f μ)
α : Type u_2
β : Type u_3
γ✝ : Type ?u.350679
ι : Type ?u.350682
inst✝² : Countable ι
m : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ✝
f✝ g✝ : α → β
γ : Type u_1
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
⊢ AEStronglyMeasurable g (Measure.map f μ) ↔ AEStronglyMeasurable (g ∘ f) μ
refine' ⟨fun H => H.comp_measurable hf.measurable, _⟩
case intro.intro
α : Type u_2
β : Type u_3
γ✝ : Type ?u.350679
ι : Type ?u.350682
inst✝² : Countable ι
m : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ✝
f✝ g✝ : α → β
γ : Type u_1
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
g₁ : γ → β
hgm₁ : StronglyMeasurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
⊢ AEStronglyMeasurable g (Measure.map f μ)
α : Type u_2
β : Type u_3
γ✝ : Type ?u.350679
ι : Type ?u.350682
inst✝² : Countable ι
m : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ✝
f✝ g✝ : α → β
γ : Type u_1
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
⊢ AEStronglyMeasurable (g ∘ f) μ → AEStronglyMeasurable g (Measure.map f μ)
rintro ⟨g₁, hgm₁, heq⟩
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
γ✝ : Type ?u.350679
ι : Type ?u.350682
inst✝² : Countable ι
m : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ✝
f✝ g✝ : α → β
γ : Type u_1
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g g₂ : α → β
hgm₂ : StronglyMeasurable g₂
hgm₁ : StronglyMeasurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEStronglyMeasurable g (Measure.map f μ)
case intro.intro
α : Type u_2
β : Type u_3
γ✝ : Type ?u.350679
ι : Type ?u.350682
inst✝² : Countable ι
m : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ✝
f✝ g✝ : α → β
γ : Type u_1
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
g₁ : γ → β
hgm₁ : StronglyMeasurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
⊢ AEStronglyMeasurable g (Measure.map f μ)
rcases hf.exists_stronglyMeasurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩
no goals
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
γ✝ : Type ?u.350679
ι : Type ?u.350682
inst✝² : Countable ι
m : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ✝
f✝ g✝ : α → β
γ : Type u_1
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g g₂ : α → β
hgm₂ : StronglyMeasurable g₂
hgm₁ : StronglyMeasurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEStronglyMeasurable g (Measure.map f μ)
exact ⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩