English
If each T_i is a topological basis on X_i, then the induced basis on the infimum (product) topology is again a topological basis, with basic sets given by finite intersections of pullbacks of U_i from T_i.
Русский
Если каждый T_i — базис на X_i, то индуцированный базис на инфимуме (произведении) снова является базисом, основы которого задаются конечными пересечениями выведенных из T_i множеств.
LaTeX
$$$\\forall i,\\mathsf{IsTopologicalBasis}(T_i) \\Rightarrow \\mathsf{IsTopologicalBasis}\\left(\\{S: \\exists U: \\forall i, S_i, \\;\\exists F: Finset, (\\forall i\\in F, U_i\\in T_i) \\wedge S = \\bigcap_{i\\in F} f_i^{-1}(U_i)\\}\\right)$$$
Lean4
instance [SeparableSpace α] {r : α → α → Prop} : SeparableSpace (Quot r) :=
isQuotientMap_quot_mk.separableSpace
