proposition: Lemma subspace_continuous_char (Y : TopologicalSpace) (f : Y -> SubspaceTopology) : continuous f <-> continuous (compose subspace_inc f).
proof: Proof. apply weak_topology1_continuous_char. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)