try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
qed.
-interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
+interpretation "downarrow" 'downarrow a = (fun_1 ?? (downarrow ?) a).
definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
intros; constructor 1;
| intros; apply (.= (†H)‡(†H1)); apply refl1]
qed.
-interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
+interpretation "ffintersects" 'fintersects U V = (fun1 ??? (ffintersects ?) U V).
*)
record formal_topology: Type ≝
- { bt:> BTop;
- converges: ∀U,V: bt. A ? (U ↓ V) = (A ? U ∧ A ? V)
+ { bt:> OBTop;
+ converges: ∀U,V: bt. oA bt (U ↓ V) = (oA ? U ∧ oA ? V)
}.
(*
| intros; apply (.= (†H)‡(†H1)); apply refl1]
qed.
-interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
+interpretation "ffintersects'" 'fintersects U V = (fun1 ??? (ffintersects' ?) U V).
*)
record formal_map (S,T: formal_topology) : Type ≝
{ cr:> continuous_relation_setoid S T;