typos

Author: affeldt-aist

theories/topology.v

@@ -117,12 +117,12 @@ Require Import mathcomp_extra reals signed.
 (*                                     predicates on natural numbers that are *)
 (*                                     eventually true.                       *)
 (*   separates_points_from_closed f == For a closed set U and point x outside *)
-(*                                     some member of the family `f` sends    *)
-(*                                     f_i(x) outside (closure (f_i@` U)).    *)
-(*                                     used together with `join_product`      *)
-(*                   join_product f == The function (x i => f i x). When the  *)
+(*                                     some member of the family f sends      *)
+(*                                     f_i(x) outside (closure (f_i @` U)).   *)
+(*                                     Used together with join_product.       *)
+(*                   join_product f == The function (x => f ^~ x). When the   *)
 (*                                     family f separates points from closed  *)
-(*                                     sets, join_product is an embedding     *)
+(*                                     sets, join_product is an embedding.    *)
 (*                                                                            *)
 (* * Near notations and tactics:                                              *)
 (*   --> The purpose of the near notations and tactics is to make the         *)
@@ -3213,7 +3213,7 @@ Qed.
 Definition hausdorff_accessible : hausdorff_space T -> accessible_space.
 Proof.
 rewrite open_hausdorff => hsdfT => x y /hsdfT [[U V] [xU yV]] [/= ? ? /eqP].
-rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //. 
+rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //.
 by rewrite inE; apply: VUc; rewrite -inE.
 Qed.
 
@@ -6542,21 +6542,20 @@ Qed.
 End SubspaceWeak.
 
 Definition separates_points_from_closed {I : Type} {T : topologicalType}
-    {U_ : I -> topologicalType} (f_ : forall i, (T -> U_ i)) :=
+    {U_ : I -> topologicalType} (f_ : forall i, T -> U_ i) :=
   forall (U : set T) x,
   closed U -> ~ U x -> exists i, ~ (closure (f_ i @` U)) (f_ i x).
 
-(* A handy technique for emebdding a space T into a product. The key interface
-   is 'separates_points_from_closed', which guarantees that the topologies 
+(* A handy technique for embedding a space T into a product. The key interface
+   is 'separates_points_from_closed', which guarantees that the topologies
    - T's native topology
    - sup (weak f_i) - the sup of all the weak topologies of f_i
    - weak (x => (f_1 x, f_2 x,...)) - the weak topology from the product space
   are equivalent (the last equivalence seems to require accessible_space).
 *)
 Section product_embeddings.
-Context {I : choiceType} {T : topologicalType}.
-Context {U_ : I -> topologicalType}.
-Variable (f_ : forall i, (T -> U_ i)).
+Context {I : choiceType} {T : topologicalType} {U_ : I -> topologicalType}.
+Variable (f_ : forall i, T -> U_ i).
 
 Hypothesis sepf : separates_points_from_closed f_.
 Hypothesis ctsf : forall i, continuous (f_ i).
@@ -6576,7 +6575,7 @@ move=> FF; split.
 move/cvg_sup => wiFx U; rewrite /= nbhs_simpl nbhsE => [[B [[oB ?]]]].
 move/filterS; apply; have [//|i nclfix] := @sepf _ x (open_closedC oB).
 apply: (wiFx i); have /= -> := @nbhsE (weak_topologicalType (f_ i)) x.
-exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); repeat split => //.
+exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); split; [split=>//|].
   apply: open_comp; last by rewrite ?openC; last apply: closed_closure.
   by move=> + _; exact: weak_continuous.
 rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB.
@@ -6596,7 +6595,7 @@ rewrite predeqE => A; rewrite ?openE /interior.
 by split => + z => /(_ z); rewrite weak_sep_nbhsE.
 Qed.
 
-Definition join_product (x : T) : PU := fun i => f_ i x.
+Definition join_product (x : T) : PU := f_ ^~ x.
 
 Lemma join_product_continuous : continuous join_product.
 Proof.
@@ -6610,21 +6609,22 @@ apply: open_comp => // + _; rewrite /cvg_to => x U.
 by rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf.
 Qed.
 
-Lemma join_product_open : forall (A : set T), open A -> 
-  open ((join_product @` A) : set (subspace (join_product @` setT))).
+Lemma join_product_open (A : set T) : open A ->
+  open ((join_product @` A) : set (subspace (range join_product))).
 Proof.
-move=> A oA; rewrite openE => y /= [x Ax] jxy.
+move=> oA; rewrite openE => y /= [x Ax] jxy.
 have [// | i nAfiy] := @sepf (~` A) x (open_closedC oA).
 pose B := prod_topo_apply i @^-1` (~` closure (f_ i @` ~` A)).
-apply: (@filterS _ _ _ ((join_product @` setT) `&` B)). 
+apply: (@filterS _ _ _ (range join_product `&` B)).
   move=> z [[w ?]] wzE Bz; exists w => //.
   move: Bz; rewrite /B -wzE closureC; case=> K [oK KsubA] /KsubA.
   have -> : prod_topo_apply i (join_product w) = f_ i w by [].
   by move=> /exists2P/forallNP/(_ w)/not_andP [] // /contrapT.
 apply: open_nbhs_nbhs; split; last by rewrite -jxy.
-apply: openI; first exact: open_subspaceT; apply: open_subspaceW. 
-apply: open_comp; first by move=> + _; exact: prod_topo_apply_continuous.
-by exact/closed_openC/closed_closure.
+apply: openI; first exact: open_subspaceT.
+apply: open_subspaceW; apply: open_comp.
+ by move=> + _; exact: prod_topo_apply_continuous.
+exact/closed_openC/closed_closure.
 Qed.
 
 Lemma join_product_inj : accessible_space T -> set_inj [set: T] join_product.