α : Type u_3
β : Type ?u.1524783
γ : Type ?u.1524786
γ₂ : Type ?u.1524789
δ : Type u_2
ι✝ : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : CompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : Set ι
f : ι → δ → α
hs : Set.Countable s
hf : ∀ (i : ι), Measurable (f i)
this : Encodable ↑s
⊢ Measurable fun b => ⨆ (i : ι) (_ : i ∈ s), f i b
α : Type u_3
β : Type ?u.1524783
γ : Type ?u.1524786
γ₂ : Type ?u.1524789
δ : Type u_2
ι✝ : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : CompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : Set ι
f : ι → δ → α
hs : Set.Countable s
hf : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun b => ⨆ (i : ι) (_ : i ∈ s), f i b
haveI : Encodable s := hs.toEncodable
α : Type u_3
β : Type ?u.1524783
γ : Type ?u.1524786
γ₂ : Type ?u.1524789
δ : Type u_2
ι✝ : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : CompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : Set ι
f : ι → δ → α
hs : Set.Countable s
hf : ∀ (i : ι), Measurable (f i)
this : Encodable ↑s
⊢ Measurable fun b => ⨆ (x : { i // i ∈ s }), f (↑x) b
α : Type u_3
β : Type ?u.1524783
γ : Type ?u.1524786
γ₂ : Type ?u.1524789
δ : Type u_2
ι✝ : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : CompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : Set ι
f : ι → δ → α
hs : Set.Countable s
hf : ∀ (i : ι), Measurable (f i)
this : Encodable ↑s
⊢ Measurable fun b => ⨆ (i : ι) (_ : i ∈ s), f i b
simp only [iSup_subtype']
no goals
α : Type u_3
β : Type ?u.1524783
γ : Type ?u.1524786
γ₂ : Type ?u.1524789
δ : Type u_2
ι✝ : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : BorelSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : BorelSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : MeasurableSpace δ
inst✝² : CompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : Set ι
f : ι → δ → α
hs : Set.Countable s
hf : ∀ (i : ι), Measurable (f i)
this : Encodable ↑s
⊢ Measurable fun b => ⨆ (x : { i // i ∈ s }), f (↑x) b
exact measurable_iSup fun i => hf i