proposition: Lemma Rhull_smallest A : [set` Rhull A] = smallest (@is_interval R) A.
proof: Proof. apply/seteqP; split; last first. by apply: smallest_sub; [apply: interval_is_interval | apply: sub_Rhull]. move=> x /= + I [Iitv AI]; rewrite /Rhull. have [|] := asboolP (has_lbound A) => lA; last first. have /forallNP/(_ x)/existsNP[a] := lA. move=> /existsNP[Aa /negP]; rewrite -ltNge => ax. have [|]:= asboolP (has_ubound A) => uA; last first. move=> ?; have /forallNP/(_ x)/existsNP[b] := uA. move=> /existsNP[Ab /negP]; rewrite -ltNge => xb. have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. by rewrite ax xb. have [As|NAs]/= := asboolP (A _) => xA. by apply: (Iitv a (sup A)); by [apply: AI | rewrite ltW ?ax]. have [||b Ab xb] := @sup_gt _ A x; do ?by [exists a | rewrite (itvP xA)]. have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. by rewrite ax xb. have [|]:= asboolP (has_ubound A) => uA; last first. have /forallNP/(_ x)/existsNP[b] := uA. move=> /existsNP[Ab /negP]; rewrite -ltNge => xb. have [Ai|NAi]/= := asboolP (A _) => xA. by apply: (Iitv (inf A) b); by [apply: AI | rewrite (ltW xb)]. have [||a Aa ax] := @inf_lt _ A x; do ?by [exists b | rewrite (itvP xA)]. have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. by rewrite ax xb. have [Ai|NAi]/= := asboolP (A _); have [As|NAs]/= := asboolP (A _). - by apply: Iitv; apply: AI. - move=> xA. have [||b Ab xb] := @sup_gt _ A x; do ?by [exists (inf A) | rewrite (itvP xA)]. have /(_ (inf A) b) := Iitv; apply; do ?by apply: AI. by rewrite (itvP xA) (ltW xb). - move=> xA. have [||a Aa ax] := @inf_lt _ A x; do ?by [exists (sup A) | rewrite (itvP xA)]. have /(_ a (sup A)) := Iitv; apply; do ?by apply: AI. by rewrite (itvP xA) (ltW ax). have [->|/set0P AN0] := eqVneq A set0. by rewrite inf0 sup0 itv_ge//= ltBSide/= ltxx. move=> xA. have [||a Aa ax] := @inf_lt _ A x; do ?by [|rewrite (itvP xA)]. have [||b Ab xb] := @sup_gt _ A x; do ?by [|rewrite (itvP xA)]. have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. by rewrite ax xb. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) HB(structures) reals ereal signed topology normedtype sequences