diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2d85fdc0a5..2a9790a104 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -234,6 +234,9 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in file `lebesgue_Rintegral.v`,
+  + new lemma `Rdominated_cvg`.
+
 ### Changed
 
 - in `realsum.v`:
diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index 82c8feb1e5..4e9b1dc145 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
@@ -247,3 +247,46 @@ End Rintegral_lebesgue_measure.
 Notation Rintegral_itv_bndo_bndc := Rintegral_itvbo_itvbc (only parsing).
 #[deprecated(since="mathcomp-analysis 1.17.0", use=Rintegral_itvob_itvcb)]
 Notation Rintegral_itv_obnd_cbnd := Rintegral_itvob_itvcb (only parsing).
+
+Section Rdominated_convergence.
+Context d (T : measurableType d) (R : realType).
+Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
+Variables (f_ : (T -> R)^nat) (f g : T -> R).
+Hypothesis mf_ : forall n, measurable_fun D (f_ n).
+Hypothesis f_f : forall x, D x -> f_ ^~ x @ \oo --> f x.
+Hypothesis ig : integrable.body mu D (EFin \o g).
+Hypothesis absfg : forall n x, D x -> `|f_ n x| <= g x.
+
+Let mf_e n : measurable_fun D (EFin \o f_ n).
+Proof. by apply/measurable_EFinP. Qed.
+
+Let f_fe (x : T) : D x -> (f_ n x)%:E @[n --> \oo] --> (f x)%:E.
+Proof.
+move=> Dx.
+apply/fine_cvgP; split; first by apply: nearW.
+by apply: f_f.
+Qed.
+
+Let egi (x : T) : (g x)%:E \is a fin_num.
+Proof. by []. Qed.
+
+Let absfge (n : nat) (x : T) : D x -> (`|(f_ n x)%:E| <= (g x)%:E)%E.
+Proof.
+move=> Dx.
+rewrite abse_EFin lee_fin.
+by apply: absfg.
+Qed.
+
+Let mf : measurable_fun D (EFin \o f).
+Proof. by apply: emeasurable_fun_cvg; first by exact: mf_e. Qed.
+
+Lemma Rdominated_cvg : \int[mu]_(x in D) f_ n x @[n \oo] --> \int[mu]_(x in D) f x.
+Proof.
+rewrite /Rintegral.
+have := dominated_convergence mD mf_e mf (aeW _ f_fe) ig (aeW _ (fun x n Dx => absfge n Dx)).
+move=> /= [i_f _ +].
+rewrite -[X in _ --> X]fineK; first by apply: integrable_fin_num.
+by move/fine_cvg.
+Qed.
+
+End Rdominated_convergence.
\ No newline at end of file