SQUASH: Wrap a long line in Homeomorphisms

Squash into the redefinition of homeo. etc.

Author: Columbus240

theories/Topology/Homeomorphisms.v

@@ -118,8 +118,10 @@ Definition topological_property (P : TopologicalSpace -> Prop) :=
 (** a lemma to prove [topological_property] more easily, with less
   boilerplate *)
 Lemma topological_property_prover (P : TopologicalSpace -> Prop) :
-  (forall (X Y : TopologicalSpace) (f : X -> Y) (Hf : continuous f) (g : Y -> X) (Hg : continuous g)
-         (Hfg : inverse_map f g) (HX : P X), P Y) ->
+  (forall (X Y : TopologicalSpace)
+     (f : X -> Y) (Hf : continuous f)
+     (g : Y -> X) (Hg : continuous g)
+     (Hfg : inverse_map f g) (HX : P X), P Y) ->
   topological_property P.
 Proof.
   intros H.