Theorem SeparationQuotient.quotientMap_prodMap_mk

Modification history

2024-10-23 02:43

Mathlib/Topology/Inseparable.lean

chore: Rename `QuotientMap` to `IsQuotientMap` (#18062) …

Deleted SeparationQuotient.quotientMap_prodMap_mk View on Github →

2024-10-07 17:59

Mathlib/Topology/Inseparable.lean

chore(Topology): rename some `prod_map`/`prod` to `prodMap` (#17472) …

Modified SeparationQuotient.quotientMap_prodMap_mk View on Github →

2024-04-24 08:44

Mathlib/Topology/Inseparable.lean

feat(Inseparable): `Prod.map mk mk` is a quotient map (#12327) …

Added SeparationQuotient.quotientMap_prodMap_mk View on Github →