add itv_closureE, itv_interiorE, and helper lemmas

CHANGELOG_UNRELEASED.md

@@ -3,6 +3,24 @@
 ## [Unreleased]
 
 ### Added
+- in classical_sets.v
+  + lemma `powerset0`, `powerset1`, `powerset2`, `powersetS`,
+    `setorder_itv_setUl_image`, `setorder_itv_setUr_image`,
+    `setorder_itv_setDl_image`
+
+- in set_interval.v
+  + lemmas `itv_open_endsPn`, `itv_closed_endsPn`, `itv_open_ends_boundlr`,
+    `setUitv2`, `setDitv2`, `setDitvoo`, `setDitvoy`, `setDitvNyo`,
+    `setDccitv`, `setDcitvy`, `setDcitvNy`
+
+- in topology_structure.v
+  + lemmas `closureEbigcap_itvcy`,`interiorEbigcup_itvNyc`,
+    `closureEbigcap_itvcc`,`interiorEbigcup_itvcc`
+
+- in num_topology.v
+  + lemmas `open_itv_open_ends`, `closed_itv_closed_ends`,
+    `itv_closureE`, `itv_interiorE`
+
 - in order_topology.v
   + lemma `itv_closed_ends_closed`
 - in classical_sets.v
@@ -22,6 +40,9 @@
   + lemmas `pmf_gt0_countable`, `pmf_measurable`
 
 ### Changed
+- in set_interval.v
+  + `setDitv1l`, `setDitv1r` (generalized)
+
 - in set_interval.v
   + `itv_is_closed_unbounded` (fix the definition)
 

classical/classical_sets.v

@@ -218,6 +218,8 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Declare Scope classical_set_scope.
+Declare Scope relation_scope.
+Delimit Scope relation_scope with relation.
 
 Reserved Notation "[ 'set' x : T | P ]" (only parsing).
 Reserved Notation "[ 'set' x | P ]" (format "[ 'set'  x  |  P ]").
@@ -3339,14 +3341,12 @@ Proof. by apply/seteqP; split; move=> x/=; rewrite /ysection/= inE. Qed.
 
 End section.
 
-Declare Scope relation_scope.
-Delimit Scope relation_scope with relation.
-
 Notation "B \; A" :=
   ([set xy | exists2 z, A (xy.1, z) & B (z, xy.2)]) : relation_scope.
 
 Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : relation_scope.
 
+Section relation.
 Local Open Scope relation_scope.
 
 Lemma set_compose_subset {X Y : Type} (A C : set (X * Y)) (B D : set (Y * X)) :
@@ -3370,4 +3370,57 @@ Definition diagonal {T : Type} := [set x : T * T | x.1 = x.2].
 Lemma diagonalP {T : Type} (x y : T) : diagonal (x, y) <-> x = y.
 Proof. by []. Qed.
 
-Local Close Scope relation_scope.
+End relation.
+
+Lemma powerset0 {T : Type} :
+  [set X | X `<=` set0] = [set set0] :> set (set T).
+Proof. by apply/funext => X /=; rewrite subset0. Qed.
+
+Lemma powerset1 {T : Type} (a : T) :
+  [set X | X `<=` [set a]] = [set set0; [set a]].
+Proof. by apply/seteqP; split => X/=; [move/subset_set1|case=> ->]. Qed.
+
+Lemma powerset2 {T : Type} (a b : T) :
+  [set X | X `<=` [set a; b]] = [set set0; [set a]; [set b]; [set a; b]].
+Proof.
+apply/seteqP; split => X/=; first by move/subset_set2; rewrite or4E !orA.
+by move=> [[[]|]|] ->.
+Qed.
+
+Lemma powersetS {T : Type} (A B : set T) :
+  (A `<=` B) = ([set X | X `<=` A] `<=` [set X | X `<=` B]).
+Proof.
+apply: propext; split; first by move=> AB X/= /subset_trans; apply.
+by move=> + a Aa => /(_ [set a])/= /(_ _ a); apply => // ? ->.
+Qed.
+
+Lemma setorder_itv_setUl_image {T : Type} (A B : set T) :
+  A `<=` B ->
+  `[A, B]%classic = (setU A) @` [set X | X `<=` B `\` A].
+Proof.
+move=> AB; apply/seteqP; split => Y/=.
+  rewrite in_itv/= => /andP[]; rewrite !subsetEset => AY YB.
+  by exists (Y `\` A); [exact: setSD | rewrite setDUK].
+case=> X XBA <-; rewrite in_itv/= Order.JoinTheory.leUl/=.
+by rewrite -(setDUK AB) Order.JoinTheory.leU2// subsetEset.
+Qed.
+
+Lemma setorder_itv_setUr_image {T : Type} (A B : set T) :
+  A `<=` B ->
+  `[A, B]%classic = (setU^~ A) @` [set X | X `<=` B `\` A].
+Proof.
+by (under eq_imagel do rewrite setUC); exact: setorder_itv_setUl_image.
+Qed.
+
+Lemma setorder_itv_setDl_image {T : Type} (A B : set T) :
+  A `<=` B ->
+  `[A, B]%classic = (setD B) @` [set X | X `<=` B `\` A].
+Proof.
+move=> AB; apply/seteqP; split => Y/=.
+  rewrite in_itv/= => /andP[]; rewrite !subsetEset => AY YB.
+  by exists (B `\` Y); [exact: setDS | rewrite setDD setIidr].
+case=> X XBA <-; rewrite in_itv/= Order.MeetTheory.leIl andbT.
+rewrite (@Order.POrderTheory.le_trans _ _ (B `\` (B `\` A)))//; last first.
+  by rewrite subsetEset; exact: setDS.
+by rewrite setDD setIidr.
+Qed.

classical/set_interval.v

@@ -55,10 +55,7 @@ Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).
 Definition neitv i := [set` i] != set0.
 
 Lemma neitv_lt_bnd i : neitv i -> (i.1 < i.2)%O.
-Proof.
-case: i => a b; apply: contraNT => /= /itv_ge ab0.
-by apply/eqP; rewrite predeqE => t; split => //=; rewrite ab0.
-Qed.
+Proof. case: i => a b /set0P[] ?; exact: itv_boundlr_lt. Qed.
 
 Lemma set_itvP i j : [set` i] = [set` j] :> set _ <-> i =i j.
 Proof.
@@ -182,38 +179,66 @@ Definition set_itvE := (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo,
 Lemma set_itvxx a : [set` Interval a a] = set0.
 Proof. by move: a => [[|] a |[|]]; rewrite !set_itvE. Qed.
 
-Lemma setUitv1 a x : (a <= BLeft x)%O ->
-  [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].
+Let setUitv1_gen a x b : (a <= BLeft x)%O ->
+  [set` Interval a (BSide b x)] `|` [set x] = [set` Interval a (BRight x)].
 Proof.
-move=> ax; apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE.
+move=> ax; case: b; last first.
+  by apply: setUidl => ? /= ->; rewrite itv_boundlr ax lexx.
+apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE.
 by rewrite (rwP eqP) (rwP orP) orbC.
 Qed.
 
+Let setU1itv_gen a x b : (BRight x <= a)%O ->
+  x |` [set` Interval (BSide b x) a] = [set` Interval (BLeft x) a].
+Proof.
+move=> ax; case: b.
+  by apply: setUidr => ? /= ->; rewrite itv_boundlr ax lexx.
+apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE.
+by rewrite (rwP eqP) (rwP orP) orbC.
+Qed.
+
+Lemma setUitv1 a x : (a <= BLeft x)%O ->
+  [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].
+Proof. exact: setUitv1_gen. Qed.
+
 Lemma setU1itv a x : (BRight x <= a)%O ->
   x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a].
+Proof. exact: setU1itv_gen. Qed.
+
+Lemma setUitv2 x y b1 b2 :
+  (x <= y)%O ->
+  [set` Interval (BSide b1 x) (BSide b2 y)] `|` [set x; y] = `[x, y]%classic.
 Proof.
-move=> ax; apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE.
-by rewrite (rwP eqP) (rwP orP) orbC.
+rewrite le_eqVlt => /orP [/eqP->|xy].
+  by case: b1; case: b2; rewrite !set_itvE !setUid // set0U.
+rewrite setUCA setUitv1_gen; last by case: b1; rewrite bnd_simp// ltW.
+by rewrite setU1itv_gen// bnd_simp ltW.
 Qed.
 
-Lemma setDitv1r a x :
-  [set` Interval a (BRight x)] `\ x = [set` Interval a (BLeft x)].
+Lemma setDitv1r a x b :
+  [set` Interval a (BSide b x)] `\ x = [set` Interval a (BLeft x)].
 Proof.
+case: b; first by apply: not_setD1; rewrite /= in_itv/= ltxx andbF.
 apply/seteqP; split => [z|z] /=; rewrite !in_itv/=.
   by move=> [/andP[-> /= zx] /eqP xz]; rewrite lt_neqAle xz.
 by rewrite lt_neqAle => /andP[-> /andP[/eqP ? ->]].
 Qed.
 
-Lemma setDitv1l a x :
-  [set` Interval (BLeft x) a] `\ x = [set` Interval (BRight x) a].
+Lemma setDitv1l a x b :
+  [set` Interval (BSide b x) a] `\ x = [set` Interval (BRight x) a].
 Proof.
+case: b; last by apply: not_setD1; rewrite /= in_itv/= ltxx.
 apply/seteqP; split => [z|z] /=; rewrite !in_itv/=.
   move=> [/andP[xz ->]]; rewrite andbT => /eqP.
   by rewrite lt_neqAle eq_sym => ->.
 move=> /andP[]; rewrite lt_neqAle => /andP[xz zx ->].
 by rewrite andbT; split => //; exact/nesym/eqP.
 Qed.
 
+Lemma setDitv2 x y b1 b2 :
+  [set` Interval (BSide b1 x) (BSide b2 y)] `\` [set x; y] = `]x, y[%classic.
+Proof. by rewrite -setDDl setDitv1l setDitv1r. Qed.
+
 End set_itv_porderType.
 Arguments neitv {disp T} _.
 #[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `set_itvNyy`")]
@@ -314,6 +339,96 @@ move=> cab; apply/seteqP; split => [x /= [xab /eqP]|x[|]]/=.
   by apply/eqP; rewrite gt_eqF.
 Qed.
 
+Lemma setDitvoo (x y : T) (b1 b2 : bool) :
+  neitv (Interval (BSide b1 x) (BSide b2 y)) ->
+  [set` Interval (BSide b1 x) (BSide b2 y)] `\` `]x, y[ =
+  (if b1 then [set x] else set0) `|` (if b2 then set0 else [set y]).
+Proof.
+move=> /neitv_lt_bnd/= xy.
+apply/seteqP; split => z/=; rewrite !in_itv/=; last first.
+  move: b1 b2 xy.
+  case=> -[]; rewrite !bnd_simp/= => + []// -> => ->; rewrite ?lexx ?ltxx//.
+  by rewrite andbF.
+case=> /[swap] /negP; rewrite negb_and.
+move: b1 b2 {xy}.
+case=> -[]/= + /andP[]; rewrite ?ltNge !negbK => /orP[]; try move=> -> //.
+- by case; move=> ? ? ?; left; apply/le_anti/andP; split.
+- by case; move=> ? ? ?; left; apply/le_anti/andP; split.
+- by case; move=> ? ? ?; right; apply/le_anti/andP; split.
+- by case; move=> ? ? ?; right; apply/le_anti/andP; split.
+Qed.
+
+Lemma setDccitv (x y : T) (b1 b2 : bool) :
+  neitv `[x, y] ->
+  `[x, y] `\` [set` Interval (BSide b1 x) (BSide b2 y)] =
+  (if b1 then set0 else [set x]) `|` (if b2 then [set y] else set0).
+Proof.
+move=> /neitv_lt_bnd/= xy.
+apply/seteqP; split => z/=; rewrite !in_itv/=; last first.
+  move: b1 b2 xy.
+  case=> -[]; rewrite !bnd_simp/= => + []// -> => ->; rewrite ?lexx ?ltxx//.
+  by rewrite andbF.
+case=> /[swap] /negP; rewrite negb_and.
+move: b1 b2 {xy}.
+case=> -[]/= /orP[] + /andP[]; rewrite -?leNgt; try move=> /negPf -> //.
+- by move=> ? ? ?; right; apply/le_anti/andP; split.
+- by move=> ? ? ?; left; apply/le_anti/andP; split.
+- by move=> ? ? ?; right; apply/le_anti/andP; split.
+- by move=> ? ? ?; left; apply/le_anti/andP; split.
+Qed.
+
+Lemma setDitvoy a (x : T) (b : bool) :
+  neitv (Interval (BSide b x) a) ->
+  [set` Interval (BSide b x) a] `\` `]x, +oo[ =
+  (if b then [set x] else set0).
+Proof.
+case/set0P => u xau.
+apply/seteqP; split => z/=; rewrite !in_itv/=; last first.
+  move: xau; case: b; rewrite //= => /[swap] <-.
+  by case: a => [[]?|[]] /itv_boundlr_lt; rewrite /= !bnd_simp.
+clear xau; case: b; rewrite /= andbT; last by case=> /andP[] ->.
+by case=> /andP[] ? _ /negP; rewrite -leNgt => ?; apply/le_anti/andP; split.
+Qed.
+
+Lemma setDitvNyo a (x : T) (b : bool) :
+  neitv (Interval a (BSide b x)) ->
+  [set` Interval a (BSide b x)] `\` `]-oo, x[ =
+  (if b then set0 else [set x]).
+Proof.
+case/set0P => u xau.
+apply/seteqP; split => z/=; rewrite !in_itv/=; last first.
+  move: xau; case: b => //= /[swap] <-.
+  by case: a => [[]?|[]] /itv_boundlr_lt; rewrite /= !bnd_simp// andbT.
+clear xau; case: b => /=; first by case=> /andP[] _ ->.
+by case=> /andP[] _ ? /negP; rewrite -leNgt => ?; apply/le_anti/andP; split.
+Qed.
+
+Lemma setDcitvy a (x : T) (b : bool) :
+  neitv (Interval (BLeft x) a) ->
+  [set` Interval (BLeft x) a] `\` [set` Interval (BSide b x) +oo%O] =
+  (if b then set0 else [set x]).
+Proof.
+case/set0P => u xau.
+apply/seteqP; split => z/=; rewrite !in_itv/=; last first.
+  move: xau; case: b => //= /[swap] <-.
+  by case: a => [[]?|[]] /itv_boundlr_lt; rewrite /= !bnd_simp.
+clear xau; case: b; rewrite /= andbT; first by case=> /andP[] ->.
+by case=> /andP[] ? _ /negP; rewrite -leNgt => ?; apply/le_anti/andP; split.
+Qed.
+
+Lemma setDcitvNy a (x : T) (b : bool) :
+  neitv (Interval a (BRight x)) ->
+  [set` Interval a (BRight x)] `\` [set` Interval -oo%O (BSide b x)] =
+  (if b then [set x] else set0).
+Proof.
+case/set0P => u xau.
+apply/seteqP; split => z/=; rewrite !in_itv/=; last first.
+  move: xau; case: b; rewrite //= => /[swap] <-.
+  by case: a => [[]?|[]] /itv_boundlr_lt; rewrite /= !bnd_simp// andbT.
+clear xau; case: b => /=; last by case=> /andP[] _ ->.
+by case=> /andP[] _ ? /negP; rewrite -leNgt => ?; apply/le_anti/andP; split.
+Qed.
+
 End set_itv_orderType.
 
 Lemma set_itv_ge disp [T : porderType disp] [b1 b2 : itv_bound T] :
@@ -893,3 +1008,38 @@ Lemma itv_setI {d} {T : orderType d} (i j : interval T) :
 Proof.
 by rewrite eqEsubset; split => z; rewrite /in_mem/= /pred_of_itv/= lexI=> /andP.
 Qed.
+
+Lemma itv_open_endsPn {d} {T : porderType d} (l r : itv_bound T) :
+  (l < r)%O ->
+  reflect
+    (exists x : T , l = BLeft x \/ r = BRight x)
+    (~~ itv_open_ends (Interval l r)).
+Proof.
+move=> lr.
+apply: (iffP idP); last first.
+  by clear lr; case=> x [] -> //; case: l => [[] ?|[]].
+move: lr; case: l => [[] L|[]] //; case: r => [[] R|[]]//= ? ?.
+all: try (by exists L; left); by exists R; right.
+Qed.
+
+Lemma itv_closed_endsPn {d} {T : porderType d} (l r : itv_bound T) :
+  (l < r)%O ->
+  reflect
+    (exists x : T , l = BRight x \/ r = BLeft x)
+    (~~ itv_closed_ends (Interval l r)).
+Proof.
+move=> lr.
+apply: (iffP idP); last first.
+  by clear lr; case=> x [] -> //; case: l => [[] ?|[]].
+move: lr; case: l => [[] L|[]] //; case: r => [[] R|[]]//= ? ?.
+all: try (by exists L; left); by exists R; right.
+Qed.
+
+Lemma itv_open_ends_boundlr {d} {T : porderType d} (bl br : itv_bound T) (x : T) :
+  itv_open_ends (Interval bl br) ->
+  (x \in Interval bl br) = (bl < BLeft x)%O && (BRight x < br)%O.
+Proof.
+rewrite itv_boundlr !le_eqVlt.
+have [->|_] := eqVneq bl (BLeft x); first by move/itv_open_ends_lside.
+by have [->|_] := eqVneq br (BRight x); first by move/itv_open_ends_rside.
+Qed.