add itv_closureE, itv_interiorE, and helper lemmas#1848

t6s wants to merge 2 commits into

math-comp:mastermath-comp/analysis:masterfrom

t6s:real_itv_open_endst6s/analysis:real_itv_open_endsCopy head branch name to clipboard