add the Sorgenfrey line and prove its properties

Co-authored-by: @garrigue

Author: motikaku

_CoqProject

@@ -133,6 +133,7 @@ theories/all_analysis.v
 
 theories/showcase/summability.v
 theories/showcase/pnt.v
+theories/showcase/sorgenfreyline.v
 
 analysis_stdlib/Rstruct_topology.v
 analysis_stdlib/showcase/uniform_bigO.v

theories/Make

@@ -97,3 +97,4 @@ pi_irrational.v
 gauss_integral.v
 all_analysis.v
 showcase/summability.v
+showcase/sorgenfreyline.v

theories/borel_hierarchy.v

@@ -21,8 +21,10 @@ Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Theory.
 Import numFieldNormedType.Exports.
+Import numFieldTopology.Exports.
 
 Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
 
 Section Gdelta_Fsigma.
 Context {T : topologicalType}.
@@ -94,3 +96,46 @@ have /Baire : forall n, open (C n) /\ dense (C n).
   - by apply: denseI => //; apply oB.
 by rewrite -C0; exact: dense0.
 Qed.
+
+Section perfectlynormalspace.
+Context (R : realType) (T : topologicalType).
+
+Definition perfectly_normal_space (x : R) :=
+  forall E : set T, closed E -> 
+    exists f : T -> R, continuous f /\ E = f @^-1` [set x].
+
+Lemma perfectly_normal_spaceP x y : perfectly_normal_space x -> perfectly_normal_space y.
+Proof.
+move=>px E cE.
+case:(px E cE) => f [] cf ->.
+pose f' := f + cst (y - x). 
+exists f'.
+split.
+  rewrite /f'.
+  move=> z.
+  apply: continuousD.
+    exact:cf.
+  exact:cst_continuous.
+apply/seteqP.
+rewrite /f' /cst /=.
+split => z /=.
+  rewrite addrfctE => ->.
+  by rewrite subrKC.
+rewrite addrfctE.
+move/eqP.
+by rewrite eq_sym -subr_eq opprB subrKC eq_sym => /eqP.
+Qed.
+
+Definition perfectly_normal_space01 :=
+  forall E F : set T, closed E -> closed F -> [disjoint E & F] ->
+    exists f : T -> R, continuous f /\ E = f @^-1` [set 0] /\ F = f @^-1` [set 1] 
+      /\ f @` [set: T] = `[0, 1]%classic.
+
+Definition perfectly_normal_space_G_delta :=
+  normal_space T /\ forall E : set T, closed E -> Gdelta E.
+
+Lemma perfectly_normal_space01P : perfectly_normal_space <-> perfectly_normal_space01.
+Proof.
+Admitted.
+
+End perfectlynormalspace.

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -95,6 +95,22 @@ Proof. by rewrite funeqE => x /=; rewrite addr0. Qed.
 Lemma center0 : center 0 = id.
 Proof. by rewrite oppr0 shift0. Qed.
 
+Lemma centerN (x y : R) : center x (- y) = - shift x y.
+Proof. by rewrite /shift opprD. Qed.
+
+Lemma shiftN (x y : R) : shift x (- y) = - center x y.
+Proof. by rewrite /shift opprD opprK. Qed.
+
+Lemma image_centerN (E : set R) (x : R) :
+  [set center x (- y) | y in E] =[set - (shift x y) | y in E].
+Proof.
+by apply/seteqP; split => y [] u Eu <- /=; exists u => //; rewrite opprD.
+Qed.
+
+Lemma image_shiftN (E : set R) (x : R) :
+  [set shift x (- y) | y in E] = [set - (center x y) | y in E].
+Proof. by rewrite -(opprK x) image_centerN opprK. Qed.
+
 End Shift.
 Arguments shift {R} x / y.
 Notation center c := (shift (- c)).