α : Type u_1
β : Type u_2
γ : Type ?u.92448
δ : Type ?u.92451
δ' : Type ?u.92454
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
T : Set α
hT : T ⊆ ⋃ (i : ι), t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (inclusion hT ⁻¹' ⋃ (i : ι), inclusion (_ : t i ⊆ ⋃ (i : ι), t i) '' (f i ⁻¹' s))
α : Type u_1
β : Type u_2
γ : Type ?u.92448
δ : Type ?u.92451
δ' : Type ?u.92454
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
T : Set α
hT : T ⊆ ⋃ (i : ι), t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (iUnionLift t f htf T hT ⁻¹' s)
rw [preimage_iUnionLift]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.92448
δ : Type ?u.92451
δ' : Type ?u.92454
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
T : Set α
hT : T ⊆ ⋃ (i : ι), t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (inclusion hT ⁻¹' ⋃ (i : ι), inclusion (_ : t i ⊆ ⋃ (i : ι), t i) '' (f i ⁻¹' s))
exact .preimage (.iUnion fun i => .image_inclusion _ (htm _) (hfm i hs)) (measurable_inclusion _)