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





leanprover-community/mathlib,leanprover-community/mathlib