α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ Continuous (sSup {f, g})
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ Continuous (f ⊔ g)
rw [← sSup_pair]
case hs
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ ∀ (f_1 : α →o β), f_1 ∈ {f, g} → Continuous f_1
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ Continuous (sSup {f, g})
apply sSup_continuous
no goals
case hs
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ ∀ (f_1 : α →o β), f_1 ∈ {f, g} → Continuous f_1
rintro f (rfl | rfl | _) <;> assumption