mathlib

0f8d7a99 - feat(order/omega_complete_partial_order): make `continuous_hom.prod.apply` continuous (#13833)

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.