Module mathcomp.analysis.topology_theory.subtype_topology

# Subtypes of topological spaces We have two distinct ways of building topologies as subsets of a topological space `X`. One is the `subspace topology`, which is defined in `subspace_topology.v`. It builds a topology on X which 'isolates' a set A. The other, defined in this file, defines a topology on the sigma type `set_type` in the initial topology by the inclusion. Note `subspace A` has the advantage that it preserves all the algebraic structure on X, but only the local behavior A (in particular, continuity). On the other hand `set_type A` has the right global properties you'd expect for the subset topology. But you can't easily add two elements of `set_val [0, 1]`. Note the implicit coercion from sets to `set_val` from `classical_sets.v`. This file provides `set_type` with a topology, and some theory. ``` sigT_of_setX == commutes `set_type` and product topologies setX_of_sigT == commutes product and `set_type` topologies ```