mathlib

8e7028cd - feat(topology/unit_interval): abstract out material about [0,1] (#7056)

feat(topology/unit_interval): abstract out material about [0,1] (#7056) Separates out some material about `[0,1]` from `topology/path_connected.lean`, and adds a very simple tactic. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>