α : Type u_3
β : Type ?u.1649128
γ : Type ?u.1649131
γ₂ : Type ?u.1649134
δ : 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✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Type u_1
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
bdd : ∀ (x : δ), BddAbove (range fun i => f i x)
⊢ Measurable fun x => sSup (range fun i => f i x)
α : Type u_3
β : Type ?u.1649128
γ : Type ?u.1649131
γ₂ : Type ?u.1649134
δ : 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✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Type u_1
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
bdd : ∀ (x : δ), BddAbove (range fun i => f i x)
⊢ Measurable fun x => ⨆ (i : ι), f i x
change Measurable fun x => sSup (range fun i : ι => f i x)
α : Type u_3
β : Type ?u.1649128
γ : Type ?u.1649131
γ₂ : Type ?u.1649134
δ : 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✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Type u_1
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
bdd : ∀ (x : δ), BddAbove ((fun i => f i x) '' univ)
⊢ Measurable fun x => sSup ((fun i => f i x) '' univ)
α : Type u_3
β : Type ?u.1649128
γ : Type ?u.1649131
γ₂ : Type ?u.1649134
δ : 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✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Type u_1
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
bdd : ∀ (x : δ), BddAbove (range fun i => f i x)
⊢ Measurable fun x => sSup (range fun i => f i x)
simp_rw [← image_univ] at bdd⊢
no goals
α : Type u_3
β : Type ?u.1649128
γ : Type ?u.1649131
γ₂ : Type ?u.1649134
δ : 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✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Type u_1
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
bdd : ∀ (x : δ), BddAbove ((fun i => f i x) '' univ)
⊢ Measurable fun x => sSup ((fun i => f i x) '' univ)
refine' measurable_cSup countable_univ hf bdd