record topological_space : Type ≝
{ top_carrier:> Type;
top_domain:> set top_carrier;
- top_O: set (set top_carrier);
- top_is_topological_space:> is_topology ? top_domain top_O
+ O: set (set top_carrier);
+ top_is_topological_space:> is_topology ? top_domain O
}.
(*definition is_continuous_map ≝
λX,Y: topological_space.λf: X → Y.
- ∀V. V ∈ top_O Y → (f \sup -1) V ∈ top_O X.*)
+ ∀V. V ∈ O Y → (f \sup -1) V ∈ O X.*)
definition is_continuous_map ≝
λX,Y: topological_space.λf: X → Y.
- ∀V. V ∈ top_O Y → inverse_image ? ? f V ∈ top_O X.
+ ∀V. V ∈ O Y → inverse_image ? ? f V ∈ O X.
record continuous_map (X,Y: topological_space) : Type ≝
{ cm_f:> X → Y;