Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.injective.embedding_induced

Modification history

2021-12-30 08:19
src/topology/maps.lean
chore(topology/algebra/weak_dual_topology): review (#11141) …
Added function.injective.embedding_inducedView on Github →