English
Let V be a topological basis on X. If the quotient map q: X → Quotient S is an open map, then the image of V under q is a topological basis on the quotient space Quotient S.
Русский
Пусть V — топологический базис на X. если квазиобразующая карта q: X → Quotient S является открытым отображением, тогда образ V под q образует топологический базис в фактор-пространстве Quotient S.
LaTeX
$$$\text{If } V \text{ is a topological basis on } X \text{ and } q:X \to \mathrm{Quotient}(S) \text{ is an open map, then } q''V \text{ is a topological basis on } \mathrm{Quotient}(S).$$$
Lean4
/-- The image of a topological basis "downstairs" in an open quotient is a topological basis. -/
theorem quotient {V : Set (Set X)} (hV : IsTopologicalBasis V) (h : IsOpenMap (Quotient.mk' : X → Quotient S)) :
IsTopologicalBasis (Set.image (Quotient.mk' : X → Quotient S) '' V) :=
hV.isQuotientMap isQuotientMap_quotient_mk' h
