pretty-printing of {within _, continuous _}

Co-author: holgerthies

Author: affeldt-aist

theories/lebesgue_integral_theory/measurable_fun_approximation.v

@@ -758,7 +758,7 @@ exists (\bigcup_(i in range f) dK i); split.
   + move=> i _; split; first by apply: compact_closed; have [] := dkP i.
     apply: (continuous_subspaceW (dKsub i)).
     apply: (@subspace_eq_continuous _ _ _ (fun=> i)).
-      by move=> ? /set_mem ->.
+      by rewrite /from_subspace => ? /set_mem ->.
     by apply: continuous_subspaceT => ?; exact: cvg_cst.
 Qed.
 

theories/topology_theory/subspace_topology.v

@@ -303,8 +303,12 @@ Global Instance subspace_proper_filter {T : topologicalType}
     (A : set T) (x : subspace A) :
   ProperFilter (nbhs_subspace x) := nbhs_subspace_filter x.
 
+Definition from_subspace {T U : Type} (A : set T) (f : T -> U) : subspace A -> U :=
+  f.
+Arguments from_subspace {T U} A f.
+
 Notation "{ 'within' A , 'continuous' f }" :=
-  (continuous (f : subspace A -> _)) : classical_set_scope.
+  (continuous (from_subspace A f)) : classical_set_scope.
 
 Arguments nbhs_subspaceP {T} A x.