α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.79726
δ' : Type ?u.79729
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).fst
hf₂ : Measurable fun a => (f a).snd
⊢ mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.79726
δ' : Type ?u.79729
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).fst
hf₂ : Measurable fun a => (f a).snd
⊢ MeasurableSpace.comap Prod.fst mβ ≤ MeasurableSpace.map f m
rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.79726
δ' : Type ?u.79729
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).fst
hf₂ : Measurable fun a => (f a).snd
⊢ mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m
exact hf₁
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.79726
δ' : Type ?u.79729
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).fst
hf₂ : Measurable fun a => (f a).snd
⊢ mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.79726
δ' : Type ?u.79729
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).fst
hf₂ : Measurable fun a => (f a).snd
⊢ MeasurableSpace.comap Prod.snd mγ ≤ MeasurableSpace.map f m
rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.79726
δ' : Type ?u.79729
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).fst
hf₂ : Measurable fun a => (f a).snd
⊢ mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m
exact hf₂