feat(order/omega_complete_partial_order): make `continuous_hom.prod.a…

…pply` 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.

src/order/omega_complete_partial_order.lean

@@ -386,6 +386,13 @@ instance : omega_complete_partial_order (α × β) :=
   le_ωSup := λ c i,
     ⟨le_ωSup (c.map order_hom.fst) i, le_ωSup (c.map order_hom.snd) i⟩ }
 
+lemma ωSup_zip (c₀ : chain α) (c₁ : chain β) :
+  ωSup (c₀.zip c₁) = (ωSup c₀, ωSup c₁) :=
+begin
+  apply eq_of_forall_ge_iff, rintro ⟨z₁,z₂⟩,
+  simp [ωSup_le_iff, forall_and_distrib],
+end
+
 end prod
 
 open omega_complete_partial_order
@@ -644,19 +651,6 @@ of_mono (order_hom.const _ x) (continuous_const x)
 instance [inhabited β] : inhabited (α →𝒄 β) :=
 ⟨ const default ⟩
 
-namespace prod
-
-/-- The application of continuous functions as a monotone function.
-
-(It would make sense to make it a continuous function, but we are currently constructing a
-`omega_complete_partial_order` instance for `α →𝒄 β`, and we cannot use it as the domain or image
-of a continuous function before we do.) -/
-@[simps]
-def apply : (α →𝒄 β) × α →o β :=
-{ to_fun := λ f, f.1 f.2,
-  monotone' := λ x y h, by dsimp; transitivity y.fst x.snd; [apply h.1, apply y.1.monotone h.2] }
-
-end prod
 
 /-- The map from continuous functions to monotone functions is itself a monotone function. -/
 @[simps]
@@ -704,18 +698,39 @@ instance : omega_complete_partial_order (α →𝒄 β) :=
 omega_complete_partial_order.lift continuous_hom.to_mono continuous_hom.ωSup
   (λ x y h, h) (λ c, rfl)
 
+namespace prod
+
+/-- The application of continuous functions as a continuous function.  -/
+@[simps]
+def apply : (α →𝒄 β) × α →𝒄 β :=
+{ to_fun := λ f, f.1 f.2,
+  monotone' := λ x y h, by {dsimp, transitivity y.fst x.snd; [apply h.1, apply y.1.monotone h.2]},
+  cont := begin
+    intro c,
+    apply le_antisymm,
+    { apply ωSup_le, intros i,
+      dsimp,
+      rw (c _).fst.continuous,
+      apply ωSup_le, intros j,
+      apply le_ωSup_of_le (max i j),
+      apply apply_mono,
+      exact monotone_fst (order_hom.mono _ (le_max_left _ _)),
+      exact monotone_snd (order_hom.mono _ (le_max_right _ _)), },
+    { apply ωSup_le, intros i,
+      apply le_ωSup_of_le i,
+      dsimp,
+      apply order_hom.mono _,
+      apply le_ωSup_of_le i,
+      reflexivity, }
+  end }
+
+end prod
+
 lemma ωSup_def (c : chain (α →𝒄 β)) (x : α) : ωSup c x = continuous_hom.ωSup c x := rfl
 
-lemma ωSup_ωSup (c₀ : chain (α →𝒄 β)) (c₁ : chain α) :
-  ωSup c₀ (ωSup c₁) = ωSup (continuous_hom.prod.apply.comp $ c₀.zip c₁) :=
-begin
-  apply eq_of_forall_ge_iff, intro z,
-  simp only [ωSup_le_iff, (c₀ _).continuous, chain.map_coe, to_mono_coe, coe_apply,
-    order_hom.omega_complete_partial_order_ωSup_coe, ωSup_def, forall_forall_merge,
-    chain.zip_coe, order_hom.prod_map_coe, order_hom.diag_coe, prod.map_mk,
-    order_hom.apply_coe, function.comp_app, prod.apply_coe,
-    order_hom.comp_coe, ωSup_apply, function.eval],
-end
+lemma ωSup_apply_ωSup (c₀ : chain (α →𝒄 β)) (c₁ : chain α) :
+  ωSup c₀ (ωSup c₁) = prod.apply (ωSup (c₀.zip c₁)) :=
+by simp [prod.apply_apply, prod.ωSup_zip]
 
 /-- A family of continuous functions yields a continuous family of functions. -/
 @[simps]