mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

feat(Mathlib/Tactic/UnitInterval): add `unit_interval` macro

Open j-loreaux opened this issue 3 years ago • 0 comments
trafficstars

Lean 3 version: https://github.com/leanprover-community/mathlib/blob/master/src/topology/unit_interval.lean#L148

j-loreaux avatar Jul 20 '22 18:07 j-loreaux