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) : IsOpen (Set.range f)

theorem polish_of_locally_compact_second_countable (X : Type u_1) [TopologicalSpace X] [SecondCountableTopology X] [T2Space X] [LocallyCompactSpace X] : PolishSpace X