mathlib4
mathlib4 copied to clipboard
feat(Mathlib/Tactic/UnitInterval): add `unit_interval` macro
trafficstars
Lean 3 version: https://github.com/leanprover-community/mathlib/blob/master/src/topology/unit_interval.lean#L148