mathlib3

4036f521 - feat(topology/unit_interval): add lemma add_pos (#16507)

feat(topology/unit_interval): add lemma add_pos (#16507) Add `lemma add_pos` stating that for every element of the unit interval and for every positive real number, their sum (as real number) is positive It is needed for #16029 defining H-spaces