ι : Type ?u.3357463
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.3357475
R : Type ?u.3357478
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
hf : MeasurableEmbedding f
⊢ AEMeasurable (g ∘ f) → AEMeasurable g
ι : Type ?u.3357463
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.3357475
R : Type ?u.3357478
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
hf : MeasurableEmbedding f
⊢ AEMeasurable g ↔ AEMeasurable (g ∘ f)
refine' ⟨fun H => H.comp_measurable hf.measurable, _⟩
case intro.intro
ι : Type ?u.3357463
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.3357475
R : Type ?u.3357478
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
hf : MeasurableEmbedding f
g₁ : α → γ
hgm₁ : Measurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
⊢ AEMeasurable g
ι : Type ?u.3357463
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.3357475
R : Type ?u.3357478
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
hf : MeasurableEmbedding f
⊢ AEMeasurable (g ∘ f) → AEMeasurable g
rintro ⟨g₁, hgm₁, heq⟩
case intro.intro.intro.intro
ι : Type ?u.3357463
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.3357475
R : Type ?u.3357478
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
hf : MeasurableEmbedding f
g₂ : β → γ
hgm₂ : Measurable g₂
hgm₁ : Measurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEMeasurable g
case intro.intro
ι : Type ?u.3357463
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.3357475
R : Type ?u.3357478
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
hf : MeasurableEmbedding f
g₁ : α → γ
hgm₁ : Measurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
⊢ AEMeasurable g
rcases hf.exists_measurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩
no goals
case intro.intro.intro.intro
ι : Type ?u.3357463
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.3357475
R : Type ?u.3357478
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
hf : MeasurableEmbedding f
g₂ : β → γ
hgm₂ : Measurable g₂
hgm₁ : Measurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEMeasurable g
exact ⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩