case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (f : α → β), f ∈ (fun x x_1 => x '' x_1) OrderHom.toFun s → Continuous' f
⊢ Continuous' (sSup ((fun x x_1 => x '' x_1) OrderHom.toFun s))
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hc : ∀ (f : α → β), f ∈ s → Continuous' f
⊢ Continuous' (sSup s)
lift s to Set (α →o β) using fun f hf => (hc f hf).to_monotone
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (x : α →o β), x ∈ s → Continuous x
⊢ Continuous' (sSup ((fun x x_1 => x '' x_1) OrderHom.toFun s))
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (f : α → β), f ∈ (fun x x_1 => x '' x_1) OrderHom.toFun s → Continuous' f
⊢ Continuous' (sSup ((fun x x_1 => x '' x_1) OrderHom.toFun s))
simp only [Set.ball_image_iff, continuous'_coe] at hc
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (x : α →o β), x ∈ s → Continuous x
⊢ Continuous' (⨆ (a : α →o β) (_ : a ∈ s), ↑a)
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (x : α →o β), x ∈ s → Continuous x
⊢ Continuous' (sSup ((fun x x_1 => x '' x_1) OrderHom.toFun s))
rw [sSup_image]
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (x : α →o β), x ∈ s → Continuous x
⊢ Continuous (⨆ (i : α →o β) (_ : i ∈ s), i)
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (x : α →o β), x ∈ s → Continuous x
⊢ Continuous' (⨆ (a : α →o β) (_ : a ∈ s), ↑a)
norm_cast
no goals
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (x : α →o β), x ∈ s → Continuous x
⊢ Continuous (⨆ (i : α →o β) (_ : i ∈ s), i)
exact iSup_continuous fun f => iSup_continuous fun hf => hc f hf