case intro.intro
α : Type u_1
β : Type ?u.60270
γ : Type ?u.60273
δ : Type ?u.60276
δ' : Type ?u.60279
ι : Sort uι
s✝ t u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (Subtype.val '' (Subtype.val ⁻¹' u))
α : Type u_1
β : Type ?u.60270
γ : Type ?u.60273
δ : Type ?u.60276
δ' : Type ?u.60279
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set ↑s
hs : MeasurableSet s
⊢ MeasurableSet t → MeasurableSet (Subtype.val '' t)
rintro ⟨u, hu, rfl⟩
case intro.intro
α : Type u_1
β : Type ?u.60270
γ : Type ?u.60273
δ : Type ?u.60276
δ' : Type ?u.60279
ι : Sort uι
s✝ t u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (u ∩ s)
case intro.intro
α : Type u_1
β : Type ?u.60270
γ : Type ?u.60273
δ : Type ?u.60276
δ' : Type ?u.60279
ι : Sort uι
s✝ t u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (Subtype.val '' (Subtype.val ⁻¹' u))
rw [Subtype.image_preimage_coe]
no goals
case intro.intro
α : Type u_1
β : Type ?u.60270
γ : Type ?u.60273
δ : Type ?u.60276
δ' : Type ?u.60279
ι : Sort uι
s✝ t u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (u ∩ s)
exact hu.inter hs