Commit 2023-03-08 06:41 5a3268e3

View on Github →

feat: port Topology.UnitInterval (#2684) Thank goodness for continuity!? :)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UnitInterval.lean

added theorem affineHomeomorph_image_I

added def iccHomeoI

added theorem iccHomeoI_apply_coe

added theorem iccHomeoI_symm_apply_coe

added theorem projIcc_eq_one

added theorem projIcc_eq_zero

added theorem unitInterval.add_pos

added theorem unitInterval.coe_ne_one

added theorem unitInterval.coe_ne_zero

added theorem unitInterval.coe_symm_eq

added theorem unitInterval.continuous_symm

added theorem unitInterval.div_mem

added theorem unitInterval.fract_mem

added theorem unitInterval.le_one'

added theorem unitInterval.le_one

added theorem unitInterval.mem_iff_one_sub_mem

added theorem unitInterval.mul_le_left

added theorem unitInterval.mul_le_right

added theorem unitInterval.mul_mem

added theorem unitInterval.mul_pos_mem_iff

added theorem unitInterval.nonneg'

added theorem unitInterval.nonneg

added theorem unitInterval.one_mem

added theorem unitInterval.one_minus_le_one

added theorem unitInterval.one_minus_nonneg

added def unitInterval.symm

added theorem unitInterval.symm_one

added theorem unitInterval.symm_symm

added theorem unitInterval.symm_zero

added theorem unitInterval.two_mul_sub_one_mem_iff

added theorem unitInterval.zero_mem