Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-14 10:16 eb2780b6

View on Github →

feat(topology/unit_interval): add lemmas (#13344)

  • also change the statement of unit_interval.mul_mem
  • from the sphere eversion project

Estimated changes

added theorem unit_interval.div_mem
modified theorem unit_interval.mul_mem
added theorem unit_interval.one_mem
modified def unit_interval.symm
added theorem unit_interval.zero_mem