proposition: Lemma is_intervalP (X : set R) : is_interval X <-> X = [set x | x \in Rhull X].
proof: Proof. split=> [iX|->]; last exact: interval_is_interval. rewrite predeqE => x /=; split; [exact: sub_Rhull | rewrite in_itv/=]. case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=. - case: asboolP => XinfX; case: asboolP => XsupX; rewrite !(lteifF, lteifT). + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx]. rewrite le_eqVlt => /orP[/eqP -> //|xsupX]. apply: (@interior_subset [the topologicalType of R : Type]). by rewrite interval_bounded_interior // /mkset infXx. + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx supXx]. apply: (@interior_subset [the topologicalType of R : Type]). by rewrite interval_bounded_interior // /mkset infXx. + move=> /andP[infXx]; rewrite le_eqVlt => /orP[/eqP -> //|xsupX]. apply: (@interior_subset [the topologicalType of R : Type]). by rewrite interval_bounded_interior // /mkset infXx. + move=> ?; apply: (@interior_subset [the topologicalType of R : Type]). by rewrite interval_bounded_interior // /mkset infXx. - case: asboolP => XinfX; rewrite !(lteifF, lteifT, andbT). + rewrite le_eqVlt => /orP[/eqP<-//|infXx]. apply: (@interior_subset [the topologicalType of R : Type]). by rewrite interval_right_unbounded_interior. + move=> infXx; apply: (@interior_subset [the topologicalType of R : Type]). by rewrite interval_right_unbounded_interior. - case: asboolP => XsupX /=. + rewrite le_eqVlt => /orP[/eqP->//|xsupX]. apply: (@interior_subset [the topologicalType of R : Type]). by rewrite interval_left_unbounded_interior. + move=> xsupX; apply: (@interior_subset [the topologicalType of R : Type]). by rewrite interval_left_unbounded_interior. - by move=> _; rewrite (interval_unbounded_setT iX). 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