Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-19 07:54 518b5d25

View on Github →

chore(topology/bases): golf a proof (#12127) Also add function.injective_iff_pairwise_ne.

Estimated changes

Modified src/data/set/pairwise.lean

added theorem function.injective_iff_pairwise_ne

Modified src/topology/bases.lean

Modified src/topology/dense_embedding.lean

deleted theorem dense_inducing.preconnected_space