Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-10 17:05 df1337ef

View on Github →

feat(data/local_equiv,topology/local_homeomorph): add local_equiv.pi and local_homeomorph.pi (#6574)

Estimated changes

Modified src/data/equiv/local_equiv.lean

added theorem local_equiv.pi_coe

added theorem local_equiv.pi_symm

Modified src/data/set/basic.lean

added theorem set.range_dcomp

Modified src/topology/constructions.lean

added theorem continuous_at_pi

Modified src/topology/continuous_on.lean

added theorem continuous_on_pi

added theorem continuous_within_at_pi

Modified src/topology/local_homeomorph.lean

added def local_homeomorph.pi