Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 09:36 563c3643

View on Github →

chore(topology/maps): golf, use section vars (#10747) Also add quotient_map.is_closed_preimage

Estimated changes

deleted theorem inducing.continuous
deleted theorem inducing.is_open_map