Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-22 10:15 198f3e54

View on Github →

chore(topology/homeomorph): add more simp lemmas (#5069) Also use implicit arguments in some iff lemmas.

Estimated changes

Modified src/topology/algebra/module.lean

Modified src/topology/homeomorph.lean

added theorem homeomorph.apply_symm_apply

added theorem homeomorph.comp_continuous_iff'

modified theorem homeomorph.comp_continuous_iff

modified theorem homeomorph.comp_continuous_on_iff

modified theorem homeomorph.range_coe

modified theorem homeomorph.self_comp_symm

added theorem homeomorph.symm_apply_apply

modified theorem homeomorph.symm_comp_self