Commit 2021-08-03 20:19 85025718

View on Github →

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.

Estimated changes

Modified src/topology/discrete_quotient.lean

added theorem discrete_quotient.proj_bot_bijective

added theorem discrete_quotient.proj_bot_injective

Modified src/topology/subset_properties.lean

added theorem is_clopen_discrete