We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent f75d649 commit d813d75Copy full SHA for d813d75
theories/topology_theory/initial_topology.v
@@ -15,9 +15,9 @@ From mathcomp Require Import pseudometric_structure.
15
(* respect to $f$. *)
16
(* *)
17
(* NB: Before version 1.16.0, the initial topology was called the weak *)
18
-(* topology. Though in some literature it can be called that way, we reserve *)
19
-(* "weak topology" for the topology induced on a topological vector space by *)
20
-(* its dual. *)
+(* topology. Though in some literature (e.g., Wilansky) it can be called that *)
+(* way, we reserve "weak topology" for the topology induced on a topological *)
+(* vector space by its dual. *)
21
22
(* ``` *)
23
(* initial_topology f == initial topology by a function f : S -> T on S *)
0 commit comments