generalize interior_itv

CHANGELOG_UNRELEASED.md

@@ -30,14 +30,22 @@
 - in `classical_sets.v`:
   + lemmas `xsectionE`, `ysectionE`
 
+- in `topology_theory/topological_structure.v`
+  + lemmas `interiorT`, `interior0`
+
 - in `normedtype.v`:
-  + lemmas `interior_itv_bnd`, `interior_itv_bndy`, `interior_itv_Nybnd`,
-    definition `interior_itv`
+  + lemma `interior_set1`
+  + lemmas `interior_itv_bnd`, `interior_itv_bndy`, `interior_itv_Nybnd`, `interior_itv_Nyy`
+  + definition `interior_itv`
 
 - in `derive.v`:
-  + lemmas `decr_derive1_le0`, `decr_derive1_le0_itv`
-  + lemmas `ler0_derive1_nincry`, `le0r_derive1_ndecry`
-
+  + lemmas `decr_derive1_le0`, `decr_derive1_le0_itv`,
+           `decr_derive1_le0_itvy`, `decr_derive1_le0_itvNy`,
+           `incr_derive1_ge0`, `incr_derive1_ge0_itv`,
+           `incr_derive1_ge0_itvy`, `incr_derive1_ge0_itvNy`,
+  + lemmas `ler0_derive1_nincry`, `le0r_derive1_ndecry`,
+           `ler0_derive1_nincrNy`, `le0r_derive1_ndecrNy`
+
 ### Changed
 
 - in `lebesgue_integrale.v`

theories/normedtype.v

@@ -4761,10 +4761,25 @@ have /sup_adherent/(_ hsX)[f Xf] : 0 < sup X - r by rewrite subr_gt0.
 by rewrite subKr => rf; apply: (iX e f); rewrite ?ltW.
 Qed.
 
-Lemma interior_itv_bnd (x y : R) (a b : bool) : x < y ->
+Lemma interior_set1 (a : R) : [set a]^° = set0.
+Proof.
+rewrite interval_bounded_interior; first last.
+- by exists a => [?]/= ->; apply: lexx.
+- by exists a => [?]/= ->; apply: lexx.
+- by move=> ? ?/= -> -> r; rewrite -eq_le; move/eqP <-.
+- rewrite inf1 sup1 eqEsubset; split => // => x/=.
+  by rewrite ltNge => /andP[/negP + ?]; apply; apply/ltW.
+Qed.
+
+Lemma interior_itv_bnd (x y : R) (a b : bool) :
   [set` Interval (BSide a x) (BSide b y)]^° = `]x, y[%classic.
 Proof.
-move=> xy.
+have [|xy] := leP y x.
+  rewrite le_eqVlt => /predU1P[-> |yx].
+    by case: a; case: b; rewrite set_itvoo0 ?set_itvE ?interior_set1 ?interior0.
+  rewrite !set_itv_ge ?interior0//.
+  - by rewrite bnd_simp -leNgt ltW.
+  - by case: a; case: b; rewrite bnd_simp -?leNgt -?ltNge ?ltW.
 rewrite interval_bounded_interior//; last exact: interval_is_interval.
 rewrite inf_itv; last by case: a; case b; rewrite bnd_simp ?ltW.
 rewrite sup_itv; last by case: a; case b; rewrite bnd_simp ?ltW.
@@ -4793,13 +4808,10 @@ Qed.
 
 Lemma interior_itv_Nyy :
   [set` Interval (BInfty R true) (BInfty _ false)]^° = `]-oo, +oo[%classic.
-Proof.
-rewrite set_itv_infty_infty.
-exact: interiorT.
-Qed.
+Proof. by rewrite set_itv_infty_infty; apply: interiorT. Qed.
 
 Definition interior_itv :=
-  (interior_itv_bnd, interior_itv_bndy, interior_itv_Nybnd).
+  (interior_itv_bnd, interior_itv_bndy, interior_itv_Nybnd, interior_itv_Nyy).
 
 Definition Rhull (X : set R) : interval R := Interval
   (if `[< has_lbound X >] then BSide `[< X (inf X) >] (inf X)

theories/topology_theory/topology_structure.v

@@ -230,6 +230,12 @@ rewrite eqEsubset; split; first exact: interior_subset.
 by rewrite -open_subsetE//; apply: openT.
 Qed.
 
+Lemma interior0 : (@set0 T)^° = set0.
+Proof.
+rewrite eqEsubset; split; first exact: interior_subset.
+rewrite -open_subsetE//; apply: open0.
+Qed.
+
 End Topological1.
 
 Lemma open_in_nearW {T : topologicalType} (P : T -> Prop) (S : set T) :