Mathlib v3 is deprecated. Go to Mathlib v4

Theorem inducing_sigma_map

Modification history

2022-09-21 08:15

src/topology/constructions.lean

feat(topology/constructions): add/golf lemmas about `sigma` (#16571) …

Added inducing_sigma_map View on Github →