[B] Remove term "beam" in favour of "ray"

The term "ray" is used more often than "beam". For example Munkres
consistently uses "ray".
Also renames the constructors of `order_topology_subbasis`.
Also renames the lemmas about "closed intervals" to concern "closed
rays".

theories/Topology/OrderTopology.v

@@ -17,9 +17,9 @@ Definition upper_open_ray (x : X) : Ensemble X :=
  [ y : X | R x y /\ y <> x ].
 
 Inductive order_topology_subbasis : Family X :=
- | intro_lower_interval: forall x:X,
+ | intro_lower_ray: forall x:X,
  In order_topology_subbasis (lower_open_ray x)
- | intro_upper_interval: forall x:X,
+ | intro_upper_ray: forall x:X,
  In order_topology_subbasis (upper_open_ray x).
 
 Definition OrderTopology : TopologicalSpace :=
@@ -71,7 +71,7 @@ Section if_total_order.
 
 Hypothesis R_total: forall x y:X, R x y \/ R y x.
 
-Lemma lower_closed_interval_closed: forall x:X,
+Lemma lower_closed_ray_closed: forall x:X,
  closed [ y:X | R y x ].
 Proof.
 intro.
@@ -102,7 +102,7 @@ exists (upper_open_ray R x);
  now subst.
 Qed.
 
-Lemma upper_closed_interval_closed: forall x:X,
+Lemma upper_closed_ray_closed: forall x:X,
  closed [y:X | R x y].
 Proof.
 intro.

theories/Topology/RTopology.v

@@ -47,26 +47,6 @@ cut (y - z <= R_metric y z).
  apply Rle_abs.
 Qed.
 
-Lemma R_lower_beam_open : forall p,
- @open RTop [r : R | r < p].
-Proof.
-intro.
-replace [r : R | r < p] with
- [y : R | y <= p /\ y <> p] by (extensionality_ensembles; constructor; lra).
-rewrite <- family_union_singleton.
-repeat (constructor + destruct H).
-Qed.
-
-Lemma R_upper_beam_open : forall p,
- @open RTop [r : R | r > p].
-Proof.
-intro.
-replace [r : R | r > p] with
- [y : R | p <= y /\ y <> p] by (extensionality_ensembles; constructor; lra).
-rewrite <- family_union_singleton.
-repeat (constructor + destruct H).
-Qed.
-
 Lemma R_interval_open : forall p q,
  @open RTop [r : R | p < r < q].
 Proof.
@@ -135,7 +115,7 @@ split.
  apply H, Rabs_def1; simpl; lra.
 Qed.
 
-Lemma R_metric_open_ball_as_Intersection_beam (x r : R) :
+Lemma R_metric_open_ball_as_Intersection_ray (x r : R) :
  open_ball R_metric x r =
  Intersection
  (upper_open_ray Rle (x - r))
@@ -162,7 +142,7 @@ split.
  apply metric_open_ball_In; auto.
  apply R_metric_is_metric.
  }
- rewrite R_metric_open_ball_as_Intersection_beam.
+ rewrite R_metric_open_ball_as_Intersection_ray.
  apply (@open_intersection2 RTop);
  apply Hsubbasis; constructor.
 - intros U HUx.
@@ -309,13 +289,13 @@ assert (closed [x:RTop | a <= x <= b]).
  (extensionality_ensembles;
  do 2 constructor; lra).
  apply closed_intersection2.
- - apply upper_closed_interval_closed.
+ - apply upper_closed_ray_closed.
  + constructor; red; intros; auto with real.
  apply Rle_trans with y0; trivial.
  + apply OrderTopology_orders_top.
  + intros.
  destruct (total_order_T x1 y0) as [[|]|]; auto with real.
- - apply lower_closed_interval_closed.
+ - apply lower_closed_ray_closed.
  + constructor; red; intros; auto with real.
  apply Rle_trans with y0; trivial.
  + apply OrderTopology_orders_top.
@@ -600,7 +580,7 @@ destruct (bounded_real_net_has_cluster_point
 exists x0. assumption.
 Qed.
 
-Lemma RTop_subbasis_rational_beams :
+Lemma RTop_subbasis_rational_rays :
  @subbasis RTop
  (Union (ImageFamily (fun q => lower_open_ray Rle (Q2R q)))
  (ImageFamily (fun q => upper_open_ray Rle (Q2R q)))).
@@ -639,7 +619,7 @@ apply (second_countable_subbasis
  apply countable_union2;
  now apply countable_img, countable_type_ensemble, Q_countable.
 }
-apply RTop_subbasis_rational_beams.
+apply RTop_subbasis_rational_rays.
 Qed.
 
 Lemma rationals_dense_in_RTop :

theories/Topology/TietzeExtension.v

@@ -57,7 +57,7 @@ refine (
  + red.
  rewrite <- inverse_image_complement.
  apply f0_cont.
- apply lower_closed_interval_closed.
+ apply lower_closed_ray_closed.
  * apply Rle_order.
  * apply OrderTopology_orders_top.
  * intros.
@@ -73,7 +73,7 @@ refine (
  + red.
  rewrite <- inverse_image_complement.
  apply f0_cont.
- apply upper_closed_interval_closed.
+ apply upper_closed_ray_closed.
  * apply Rle_order.
  * apply OrderTopology_orders_top.
  * intros.