This is Topology.Locale/wregular_wHausdorff. A proof of this proposition can be found in Fibrewise separation axioms for locales, Peter T. Johnstone, 1990, Corollary 3.4.
This proposition requires a lot of background work since this paper is not formalized yet and it seems a lot of stuff from it is required for this proof.
This is Topology.Locale/wregular_wHausdorff. A proof of this proposition can be found in Fibrewise separation axioms for locales, Peter T. Johnstone, 1990, Corollary 3.4.
This proposition requires a lot of background work since this paper is not formalized yet and it seems a lot of stuff from it is required for this proof.