Commit 2022-05-03 14:29 0f8d7a99

feat(order/omega_complete_partial_order): make continuous_hom.prod.apply continuous (#13833) Previous it was defined as apply : (α →𝒄 β) × α →o β and the comment said that it would make sense to define it as a continuous function, but we need an instance for α →𝒄 β first. But then let’s just define that instance first, and then define apply : (α →𝒄 β) × α →𝒄 β as you would expect. Also rephrases lemma ωSup_ωSup differently now that apply is continuous.