proposition: Lemma segment_compact (a b : R) : compact `[a, b].
proof: Proof. have [leab|ltba] := lerP a b; last first. by move=> F FF /filter_ex [x abx]; move: ltba; rewrite (itvP abx). rewrite compact_cover => I D f fop sabUf. set B := [set x | exists2 E : {fset I}, {subset E <= D} & `[a, x] `<=` \bigcup_(i in [set` E]) f i /\ (\bigcup_(i in [set` E]) f i) x]. set A := `[a, b] `&` B. suff Aeab : A = `[a, b]%classic. suff [_ [E ? []]] : A b by exists E. by rewrite Aeab/= inE/=; apply/andP. apply: segment_connected. - have aba : a \in `[a, b] by rewrite in_itv /= lexx. exists a; split=> //; have /sabUf [i /= Di fia] := aba. exists [fset i]%fset; first by move=> ?; rewrite inE inE => /eqP->. split; last by exists i => //=; rewrite inE. move=> x /= aex; exists i; [by rewrite /= inE|suff /eqP-> : x == a by []]. by rewrite eq_le !(itvP aex). - exists B => //; rewrite openE => x [E sD [saxUf [i Di fx]]]. have : open (f i) by have /sD := Di; rewrite inE => /fop. rewrite openE => /(_ _ fx) [e egt0 xe_fi]; exists e => // y xe_y. exists E => //; split; last by exists i => //; apply/xe_fi. move=> z /= ayz; have [lezx|ltxz] := lerP z x. by apply/saxUf; rewrite /= in_itv/= (itvP ayz) lezx. exists i => //; apply/xe_fi; rewrite /ball_/= distrC ger0_norm. have lezy : z <= y by rewrite (itvP ayz). rewrite ltrBlDl; apply: le_lt_trans lezy _; rewrite -ltrBlDr. by have := xe_y; rewrite /ball_ => /ltr_distlCBl. by rewrite subr_ge0; apply/ltW. exists A; last by rewrite predeqE => x; split=> [[] | []]. move=> x clAx; have abx : x \in `[a, b]. by apply: interval_closed; have /closureI [] := clAx. split=> //; have /sabUf [i Di fx] := abx. have /fop := Di; rewrite openE => /(_ _ fx) [_ /posnumP[e] xe_fi]. have /clAx [y [[aby [E sD [sayUf _]]] xe_y]] := nbhsx_ballx x e%:num ltac:(by []). exists (i |` E)%fset; first by move=> j /fset1UP[->|/sD] //; rewrite inE. split=> [z axz|]; last first. exists i; first by rewrite /= !inE eq_refl. by apply/xe_fi; rewrite /ball_/= subrr normr0. have [lezy|ltyz] := lerP z y. have /sayUf [j Dj fjz] : z \in `[a, y] by rewrite in_itv /= (itvP axz) lezy. by exists j => //=; rewrite inE orbC Dj. exists i; first by rewrite /= !inE eq_refl. apply/xe_fi; rewrite /ball_/= ger0_norm; last by rewrite subr_ge0 (itvP axz). rewrite ltrBlDl -ltrBlDr; apply: lt_trans ltyz. by apply: ltr_distlCBl; rewrite distrC. 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