Polish #
Material destined for Mathlib.
theorem
open_of_locally_compact_dense_metrizable
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[T2Space X]
[TopologicalSpace Y]
[T2Space Y]
[LocallyCompactSpace Y]
(f : Y → X)
(hf : Continuous f)
(indf : Topology.IsInducing f)
(dn : DenseRange f)
:
theorem
polish_of_locally_compact_second_countable
(X : Type u_1)
[TopologicalSpace X]
[SecondCountableTopology X]
[T2Space X]
[LocallyCompactSpace X]
: