proposition: Lemma connected_intervalP (E : set R) : connected E <-> is_interval E.
proof: Proof. split => [cE x y Ex Ey z /andP[xz zy]|]. - apply: contrapT => Ez. pose Az := E `&` [set x | x < z]; pose Bz := E `&` [set x | z < x]. apply/connectedPn : cE; exists (fun b => if b then Az else Bz); split. + move: xz zy Ez. rewrite !le_eqVlt => /predU1P[<-//|xz] /predU1P[->//|zy] Ez. by case; [exists x | exists y]. + rewrite /Az /Bz -setIUr; apply/esym/setIidPl => u Eu. by apply/orP; rewrite -neq_lt; apply/negP; apply: contraPnot Eu => /eqP <-. + split; [|rewrite setIC]. + apply/disjoints_subset => /= u /closureI[_]; rewrite closure_gt => zu. by rewrite /Az setCI; right; apply/negP; rewrite -leNgt. + apply/disjoints_subset => /= u /closureI[_]; rewrite closure_lt => zu. by rewrite /Bz setCI; right; apply/negP; rewrite -leNgt. - apply: contraPP => /connectedPn[A [A0 EU sepA]] intE. have [/= x A0x] := A0 false; have [/= y A1y] := A0 true. wlog xy : A A0 EU sepA x A0x y A1y / x < y. move=> /= wlog_hypo; have [xy|yx|{wlog_hypo}yx] := ltgtP x y. + exact: (wlog_hypo _ _ _ _ _ A0x _ A1y). + apply: (wlog_hypo (A \o negb) _ _ _ y _ x) => //=; by [rewrite setUC | rewrite separatedC]. + move/separated_disjoint : sepA; rewrite predeqE => /(_ x)[] + _; apply. by split => //; rewrite yx. pose z := sup (A false `&` [set z | x <= z <= y]). have A1z : ~ (A true) z. have cA0z : closure (A false) z. suff : closure (A false `&` [set z | x <= z <= y]) z by case/closureI. apply: closure_sup; last by exists y => u [_] /andP[]. by exists x; split => //; rewrite /mkset lexx /= (ltW xy). by move: sepA; rewrite /separated => -[] /disjoints_subset + _; apply. have /andP[xz zy] : x <= z < y. rewrite sup_ub //=; [|by exists y => u [_] /andP[]|]. + rewrite lt_neqAle sup_le_ub ?andbT; last by move=> u [_] /andP[]. * by apply/negP; apply: contraPnot A1y => /eqP <-. * by exists x; split => //; rewrite /mkset /= lexx /= (ltW xy). + by split=> //; rewrite /mkset lexx (ltW xy). have [A0z|A0z] := pselect ((A false) z); last first. have {}xzy : x <= z <= y by rewrite xz ltW. have : ~ E z by rewrite EU => -[]. by apply; apply (intE x y) => //; rewrite EU; [left|right]. suff [z1 [/andP[zz1 z1y] Ez1]] : exists z1 : R, z <= z1 <= y /\ ~ E z1. apply Ez1; apply (intE x y) => //; rewrite ?EU; [by left|by right|]. by rewrite z1y (le_trans _ zz1). have [r zcA1] : {r:{posnum R}| ball z r%:num `<=` ~` closure (A true)}. have ? : ~ closure (A true) z. by move: sepA; rewrite /separated => -[] _ /disjoints_subset; apply. have ? : open (~` closure (A true)) by exact/closed_openC/closed_closure. exact/nbhsC_ball/open_nbhs_nbhs. pose z1 : R := z + r%:num / 2; exists z1. have z1y : z1 <= y. rewrite leNgt; apply/negP => yz1. suff : (~` closure (A true)) y by apply; exact: subset_closure. apply zcA1; rewrite /ball /= ltr_distl (lt_le_trans zy) // ?lerDl //. rewrite andbT ltrBlDl addrC (lt_trans yz1) // ltrD2l. by rewrite ltr_pdivrMr // ltr_pMr // ltr1n. rewrite z1y andbT lerDl; split => //. have ncA1z1 : (~` closure (A true)) z1. apply zcA1; rewrite /ball /= /z1 opprD addrA subrr add0r normrN. by rewrite ger0_norm // ltr_pdivrMr // ltr_pMr // ltr1n. have nA0z1 : ~ (A false) z1. move=> A0z1; have : z < z1 by rewrite /z1 ltrDl. apply/negP; rewrite -leNgt. apply: sup_ub; first by exists y => u [_] /andP[]. by split => //; rewrite /mkset /z1 (le_trans xz) /= ?lerDl // (ltW z1y). by rewrite EU => -[//|]; apply: contra_not ncA1z1; exact: subset_closure. 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