equal
deleted
inserted
replaced
5 theory Function_Topology |
5 theory Function_Topology |
6 imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure |
6 imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure |
7 begin |
7 begin |
8 |
8 |
9 |
9 |
10 section%important \<open>Product topology\<close> |
10 section%important \<open>Product Topology\<close> |
11 |
11 |
12 text \<open>We want to define the product topology. |
12 text \<open>We want to define the product topology. |
13 |
13 |
14 The product topology on a product of topological spaces is generated by |
14 The product topology on a product of topological spaces is generated by |
15 the sets which are products of open sets along finitely many coordinates, and the whole |
15 the sets which are products of open sets along finitely many coordinates, and the whole |