Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-26 09:22 5258669e

View on Github →

feat(topology/unit_interval): affine homeomorphisms of intervals (#7250)

Estimated changes

Modified src/data/set/intervals/image_preimage.lean

added theorem set.image_affine_Icc'

Created src/topology/algebra/field.lean

added def affine_homeomorph

Modified src/topology/unit_interval.lean

added def Icc_homeo_I

added theorem Icc_homeo_I_apply_coe

added theorem Icc_homeo_I_symm_apply_coe

added theorem affine_homeomorph_image_I