diff --git a/Lebesgue/Subset_Rbar.v b/Lebesgue/Subset_Rbar.v
index 040d3ac0cbf8784a15e7deb5e85cd03b4bd846ce..c5096fd29d7e88202f32bae3e407bc0fd9c0bc1a 100644
--- a/Lebesgue/Subset_Rbar.v
+++ b/Lebesgue/Subset_Rbar.v
@@ -422,12 +422,20 @@ Definition Rbar_oc : Rbar -> Rbar -> Rbar -> Prop :=
 Definition Rbar_oo : Rbar -> Rbar -> Rbar -> Prop :=
   fun a b => inter (Rbar_lt a) (Rbar_gt b).
 
+(** Approximations based on the Archimedean property. *)
+
+Definition Rbar_ge_eps : R -> nat -> Rbar -> Prop :=
+  fun b n => Rbar_ge (b - / (INR n + 1)).
+Definition Rbar_le_eps : R -> nat -> Rbar -> Prop :=
+  fun a n => Rbar_le (a + / (INR n + 1)).
+
 End Rbar_interval_Def.
 
 
 Ltac Rbar_interval_unfold :=
   repeat unfold
     Rbar_is_interval, Rbar_is_ray, Rbar_is_ray_l, Rbar_is_ray_r,
+    Rbar_ge_eps, Rbar_le_eps,
     Rbar_cc, Rbar_co, Rbar_oc, Rbar_oo, Rbar_ge, Rbar_gt.
 
 Ltac Rbar_interval_full_unfold :=
@@ -521,6 +529,30 @@ Proof.
 Rbar_interval_subset_intros y Hy.
 Qed.
 
+(** Open rays as countable unions of closed rays. *)
+
+Lemma Rbar_gt_is_Rbar_ge_union_seq :
+  forall (b : R), Rbar_gt b = union_seq (Rbar_ge_eps b).
+Proof.
+Rbar_interval_subset_intros y Hy; try easy.
+apply Rlt_le_minus_ex; easy.
+destruct Hy as [n Hy].
+apply Rle_lt_trans with (b - / (INR n + 1)); try easy.
+apply Rminus_lt_compat_pos, InvINRp1_pos.
+exists 0%nat; auto.
+Qed.
+
+Lemma Rbar_lt_is_Rbar_le_union_seq :
+  forall (a : R), Rbar_lt a = union_seq (Rbar_le_eps a).
+Proof.
+Rbar_interval_subset_intros y Hy; try easy.
+apply Rlt_plus_le_ex; easy.
+destruct Hy as [n Hy].
+apply Rlt_le_trans with (a + / (INR n + 1)); try easy.
+apply Rplus_lt_compat_pos, InvINRp1_pos.
+exists 0%nat; auto.
+Qed.
+
 End Rbar_ray_Facts.