Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-13 18:30 f7313156

View on Github →

feat(topology/local_homeomorph): "injectivity" local_homeomorph.prod (#15311)

Also some other lemmas about local_equiv and local_homeomorph
From the sphere eversion project

Estimated changes

Modified src/data/set/prod.lean

added theorem set.prod_eq_prod_iff

added theorem set.prod_eq_prod_iff_of_nonempty

Modified src/logic/basic.lean

added theorem forall_forall_const

Modified src/logic/equiv/local_equiv.lean

added theorem local_equiv.mem_symm_trans_source

added theorem local_equiv.trans_apply

Modified src/topology/local_homeomorph.lean

added theorem local_homeomorph.image_source_eq_target

added theorem local_homeomorph.prod_eq_prod_of_nonempty'

added theorem local_homeomorph.prod_eq_prod_of_nonempty

added theorem local_homeomorph.symm_image_target_eq_source

added theorem local_homeomorph.trans_apply