English
A second-countable space mapped by an open quotient map to a second-countable space.
Русский
Вторично счетное пространство отображается открытым отображением через квотируемое отображение в вторично счетное пространство.
LaTeX
$$$SecondCountableTopology(Y) \text{ given } IsQuotientMap(π) \text{ and } IsOpenMap(π)$$$
Lean4
/-- A second countable space is mapped by an open quotient map to a second countable space. -/
theorem _root_.Topology.IsQuotientMap.secondCountableTopology [SecondCountableTopology X] (h' : IsQuotientMap π)
(h : IsOpenMap π) : SecondCountableTopology Y where
is_open_generated_countable :=
by
obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X
exact ⟨Set.image π '' V, V_countable.image (Set.image π), (V_generates.isQuotientMap h' h).eq_generateFrom⟩
