Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-15 13:39 c8ecae8f

View on Github →

feature(analysis/topology/continuity): start homeomorphism

Estimated changes

Modified analysis/topology/continuity.lean

added theorem homeomorph.coe_eq_to_equiv

added theorem homeomorph.coinduced_eq

added theorem homeomorph.image_symm

added theorem homeomorph.induced_eq

added theorem homeomorph.preimage_symm

added def homeomorph.prod_assoc

added def homeomorph.prod_comm

added def homeomorph.prod_congr

added theorem homeomorph.range_coe

added theorem homeomorph.self_comp_symm

added theorem homeomorph.symm_comp_self

added structure homeomorph

Modified data/equiv/basic.lean

modified def equiv.prod_congr