closure of an open interval (#1910)

* closure of an open interval

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -21,6 +21,12 @@
 - in `measurable_function.v`:
   + lemma `preimage_measurability`
 
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `itv_center_shift`
+
+- in `normed_module.v`:
+  + lemmas `closure_itvoo`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:

theories/normedtype_theory/normed_module.v

@@ -2082,6 +2082,15 @@ Qed.
 
 End Closed_Ball_normedModType.
 
+(* NB: see also itv_closure *)
+Lemma closure_itvoo (R : realFieldType) (a b : R) : a < b ->
+  closure `]a, b[%classic = `[a, b]%classic.
+Proof.
+move=> ab.
+rewrite itv_center_shift// -ball_itv closure_ballE itv_center_shift//.
+by rewrite closed_ball_itv// divr_gt0// subr_gt0.
+Qed.
+
 Lemma open_subball {R : numFieldType} {M : normedModType R} (A : set M)
   (x : M) : open A -> A x -> \forall e \near 0^'+, ball x e `<=` A.
 Proof.

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -97,6 +97,16 @@ End Shift.
 Arguments shift {R} x / y.
 Notation center c := (shift (- c)).
 
+Lemma itv_center_shift {R : numFieldType} x y (a b : R) : (a < b) ->
+  let c := (a + b) / 2 in let r := (b - a) / 2 in
+  Interval (BSide x a) (BSide y b) =
+  Interval (BSide x (center r c (*c - r*) )) (BSide y (shift r c (*c + r*))).
+Proof.
+move=> ab c r; rewrite /shift /c /r -mulrBl addrKA opprK -mulrDl.
+rewrite [in X in _ = Interval _ X]addrC subrKA -!mulr2n.
+by rewrite -(mulr_natr a) -(mulr_natr b) !mulfK.
+Qed.
+
 Section at_left_right_topologicalType.
 Variables (R : numFieldType) (V : topologicalType) (f : R -> V) (x : R).