From ebe49b2d21488364203e59e1f0e76e5c063978ac Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 3 Feb 2026 17:50:52 +0900 Subject: [PATCH 1/2] better behaved Rintegral_cst --- theories/lebesgue_integral_theory/lebesgue_Rintegral.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index 916c0358a2..5f0fe74e9e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -146,7 +146,7 @@ Lemma Rintegral_set0 f : \int[mu]_(x in set0) f x = 0. Proof. by rewrite /Rintegral integral_set0. Qed. Lemma Rintegral_cst D : d.-measurable D -> - forall r, \int[mu]_(x in D) (cst r) x = r * fine (mu D). + forall r, \int[mu]_(_ in D) r = r * fine (mu D). Proof. move=> mD r; rewrite /Rintegral/= integral_cst//. have := leey (mu D); rewrite le_eqVlt => /predU1P[->/=|muy]; last first. From 716083a9db6ea5721dd2128c610c4d47ec90b8ed Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 3 Feb 2026 18:06:27 +0900 Subject: [PATCH 2/2] changelog --- CHANGELOG_UNRELEASED.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4b30c26a02..0d911f46cb 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,6 +13,9 @@ - in set_interval.v + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool) +- in `lebesgue_Rintegrable.v`: + + lemma `Rintegral_cst` (does not use `cst` anymore) + ### Renamed - in set_interval.v + `itv_is_ray` -> `itv_is_open_unbounded`