arend-lib
arend-lib copied to clipboard
Prove that strongly dense maps are closed under pullbacks along open maps
This is Topology.Locale/pullback_sdense. A proof of this lemma can be found in A constructive “Closed subgroup theorem” for localic groups and groupoids, Peter T. Johnstone, 1989, Lemma 1.9.