case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.70127
δ : Type ?u.70130
δ' : Type ?u.70133
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : Measurable fun a => f ↑a
hd : Measurable fun a => f ↑a
u : Set β
hu : MeasurableSet u
⊢ f ⁻¹' u = Subtype.val '' ((fun a => f ↑a) ⁻¹' u) ∪ Subtype.val '' ((fun a => f ↑a) ⁻¹' u)
α : Type u_1
β : Type u_2
γ : Type ?u.70127
δ : Type ?u.70130
δ' : Type ?u.70133
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : Measurable fun a => f ↑a
hd : Measurable fun a => f ↑a
u : Set β
hu : MeasurableSet u
⊢ MeasurableSet (f ⁻¹' u)
convert (hs.subtype_image (hc hu)).union (ht.subtype_image (hd hu))
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.70127
δ : Type ?u.70130
δ' : Type ?u.70133
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : Measurable fun a => f ↑a
hd : Measurable fun a => f ↑a
u : Set β
hu : MeasurableSet u
⊢ f ⁻¹' u = Subtype.val '' (Subtype.val ⁻¹' (f ⁻¹' u)) ∪ Subtype.val '' (Subtype.val ⁻¹' (f ⁻¹' u))
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.70127
δ : Type ?u.70130
δ' : Type ?u.70133
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : Measurable fun a => f ↑a
hd : Measurable fun a => f ↑a
u : Set β
hu : MeasurableSet u
⊢ f ⁻¹' u = Subtype.val '' ((fun a => f ↑a) ⁻¹' u) ∪ Subtype.val '' ((fun a => f ↑a) ⁻¹' u)
change f ⁻¹' u = (↑) '' ((↑) ⁻¹' (f ⁻¹' u) : Set s) ∪ (↑) '' ((↑) ⁻¹' (f ⁻¹' u) : Set t)
no goals
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.70127
δ : Type ?u.70130
δ' : Type ?u.70133
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : Measurable fun a => f ↑a
hd : Measurable fun a => f ↑a
u : Set β
hu : MeasurableSet u
⊢ f ⁻¹' u = Subtype.val '' (Subtype.val ⁻¹' (f ⁻¹' u)) ∪ Subtype.val '' (Subtype.val ⁻¹' (f ⁻¹' u))
rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, Subtype.range_coe,
  Subtype.range_coe, ← inter_distrib_left, univ_subset_iff.1 h, inter_univ]