feat(topology/discrete_quotient): add two lemmas (#8464)
Add lemmas `proj_bot_injective` and `proj_bot_bijective`, the former needed for the latter, and the latter needed in LTE.
Co-authored-by: Filippo A. E. Nuccio <65080144+faenuccio@users.noreply.github.com>
