proposition: Lemma interval_open a b : ~~ bound_side true a -> ~~ bound_side false b -> open [set x : R^o | x \in Interval a b].
proof: Proof. move: a b => [[]a|[]] [[]b|[]]// _ _. - have -> : [set x | a < x < b] = [set x | a < x] `&` [set x | x < b]. by rewrite predeqE => r; rewrite /mkset; split => [/andP[? ?] //|[-> ->]]. by apply openI; [exact: open_gt | exact: open_lt]. - by under eq_set do rewrite itv_ge// inE. - by under eq_set do rewrite in_itv andbT/=; exact: open_gt. - exact: open_lt. - by rewrite (_ : mkset _ = setT); [exact: openT | rewrite predeqE]. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule