From 19fc44be2a997e4a2e4f7aa5d9442c8971e6ea47 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Thu, 2 Jul 2026 10:29:11 +0200 Subject: [PATCH 1/7] added rgenopensets+changed deprecated lemmas --- .../lebesgue_integral_definition.v | 2 +- .../lebesgue_integral_fubini.v | 4 +-- theories/lebesgue_measure.v | 10 +++--- theories/measurable_realfun.v | 31 ++++++++++++++++++- 4 files changed, 38 insertions(+), 9 deletions(-) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index e4efb00d0..36492890e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -338,7 +338,7 @@ apply: cvgeZl => //=; rewrite [X in _ --> X](_ : _ = mu (\bigcup_n (f @^-1` [set r] `&` fleg c n))). by rewrite -setI_bigcupr bigcup_fleg// setIT. have ? k i : measurable (f @^-1` [set k] `&` fleg c i) by exact: measurableI. -apply: nondecreasing_cvg_mu; [by []|exact: bigcupT_measurable|]. +apply: nondecreasing_cvg_measure; [by []|exact: bigcupT_measurable|]. move=> n m nm; apply/subsetPset; apply: setIS. by move/(nd_fleg c) : nm => /subsetPset. Unshelve. all: by end_near. Qed. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index 9486051ec..ab7aec222 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -69,7 +69,7 @@ Proof. move=> F ndF; rewrite /B /= => BF; split. by apply: bigcupT_measurable => n; have [] := BF n. have phiF x : phi (F i) x @[i \oo] --> phi (\bigcup_i F i) x. - rewrite /phi /= xsection_bigcup; apply: nondecreasing_cvg_mu. + rewrite /phi /= xsection_bigcup; apply: nondecreasing_cvg_measure. - by move=> n; apply: measurable_xsection; case: (BF n). - by apply: bigcupT_measurable => i; apply: measurable_xsection; case: (BF i). - by move=> m n mn; exact/subsetPset/le_xsection/subsetPset/ndF. @@ -89,7 +89,7 @@ Proof. move=> F ndF; rewrite /B /= => BF; split. by apply: bigcupT_measurable => n; have [] := BF n. have psiF x : psi (F i) x @[i \oo] --> psi (\bigcup_i F i) x. - rewrite /psi /= ysection_bigcup; apply: nondecreasing_cvg_mu. + rewrite /psi /= ysection_bigcup; apply: nondecreasing_cvg_measure. - by move=> n; apply: measurable_ysection; case: (BF n). - by apply: bigcupT_measurable => i; apply: measurable_ysection; case: (BF i). - by move=> m n mn; exact/subsetPset/le_ysection/subsetPset/ndF. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 4894aa3f3..8d55c854e 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -630,7 +630,7 @@ Let lebesgue_measure_itvoo_subr1 (a : R) : Proof. rewrite itv_bnd_open_bigcup//; transitivity (limn (lebesgue_measure \o (fun k => `]a - 1, a - k.+1%:R^-1]%classic : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. - by move=> ?; exact: measurable_itv. - by apply: bigcup_measurable => k _; exact: measurable_itv. - move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=]. @@ -728,7 +728,7 @@ Let lebesgue_measure_itv_bnd_infty x (a : R) : Proof. rewrite itv_bndy_bigcup_BRight; transitivity (limn (lebesgue_measure \o (fun k => [set` Interval (BSide x a) (BRight (a + k%:R))] : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. + by move=> k; exact: measurable_itv. + by apply: bigcup_measurable => k _; exact: measurable_itv. + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[->/=]. @@ -744,7 +744,7 @@ Let lebesgue_measure_itv_infty_bnd y (b : R) : Proof. rewrite itvNy_bnd_bigcup_BLeft; transitivity (limn (lebesgue_measure \o (fun k => [set` Interval (BLeft (b - k%:R)) (BSide y b)] : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. + by move=> k; exact: measurable_itv. + by apply: bigcup_measurable => k _; exact: measurable_itv. + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->]. @@ -981,7 +981,7 @@ Proof. move=> mD Dfin epspos; pose Dn n := D `&` [set` `[-(n%:R), n%:R]]%R. have mDn n : measurable (Dn n) by exact: measurableI. have : mu \o Dn @ \oo --> mu (\bigcup_n Dn n). - apply: nondecreasing_cvg_mu => //. + apply: nondecreasing_cvg_measure => //. - by apply: bigcup_measurable => // ? _; exact: mDn. - move=> n m nm; apply/subsetPset; apply: setIS => z /=; rewrite !in_itv/=. move=> /andP[nz zn]; rewrite (le_trans _ nz)/= ?(le_trans zn) ?ler_nat//. @@ -1076,7 +1076,7 @@ rewrite leye_eq => /eqP /[dup] + ->. have {1}-> : D = \bigcup_n (F n `&` D) by rewrite -setI_bigcupl -RFU setTI. move=> FDp; apply/esym/eq_infty => M. have : (fun n => mu (F n `&` D)) @ \oo --> +oo. - rewrite -FDp; apply: nondecreasing_cvg_mu. + rewrite -FDp; apply: nondecreasing_cvg_measure. - by move=> i; apply: measurableI => //; exact: (ffin i).1. - by apply: bigcup_measurable => i _; exact: (measurableI _ _ (ffin i).1). - by move=> n m nm; apply/subsetPset; apply: setSI; exact/subsetPset/Fsub. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 28095e43e..1c4823619 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -497,6 +497,35 @@ Qed. End rgenopens. End RGenOpens. +Module RGenOpenSets. +Section rgenopensets. +Variable R : realType. +Implicit Types a b : R. + +Definition G := @open R. + +Lemma open_ocitv_measurable (U : set R) : G U -> measurable U. +Proof. +move=> oU; rewrite (open_disjoint_itv_bigcup oU); +apply: sigma_algebra_bigcup => k. +have /is_intervalP -> := @open_disjoint_itv_is_interval _ U oU k. +exact : measurable_itv. +Qed. + +Lemma ocitv_open_measurable a b : <> `]a,b[%classic. +Proof. by apply: sub_sigma_algebra; rewrite/G. Qed. + +Lemma measuralbeE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split; [rewrite RGenOpens.measurableE|]; + apply: sigma_algebra_subl=> U. + rewrite/RGenOpens.G/= => [[a [b ->]]]; exact: ocitv_open_measurable. +by move=> /open_ocitv_measurable. +Qed. + +End rgenopensets. +End RGenOpenSets. + Section erealwithrays. Variable R : realType. Implicit Types (x y z : \bar R) (r s : R). @@ -1729,7 +1758,7 @@ have Ek0 k : \bigcap_n (E k n) = set0. have badn' k : exists n, mu (E k n) < ((eps / 2) / (2 ^ k.+1)%:R)%:E. pose ek : R := (eps / 2 / (2 ^ k.+1)%:R)%R. have : mu \o E k @ \oo --> mu set0. - rewrite -(Ek0 k); apply: nonincreasing_cvg_mu => //. + rewrite -(Ek0 k); apply: nonincreasing_cvg_measure => //. - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []]. - exact: bigcap_measurable. rewrite measure0; case/fine_cvg/(_ (interior (ball 0%R ek))). From 541ffc43c1c685df7a59092f20649e43b4f6a5e8 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Thu, 2 Jul 2026 10:29:11 +0200 Subject: [PATCH 2/7] added rgenopensets+changed deprecated lemmas --- .../lebesgue_integral_definition.v | 2 +- .../lebesgue_integral_fubini.v | 4 +-- theories/lebesgue_measure.v | 10 +++--- theories/measurable_realfun.v | 31 ++++++++++++++++++- 4 files changed, 38 insertions(+), 9 deletions(-) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index e4efb00d0..36492890e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -338,7 +338,7 @@ apply: cvgeZl => //=; rewrite [X in _ --> X](_ : _ = mu (\bigcup_n (f @^-1` [set r] `&` fleg c n))). by rewrite -setI_bigcupr bigcup_fleg// setIT. have ? k i : measurable (f @^-1` [set k] `&` fleg c i) by exact: measurableI. -apply: nondecreasing_cvg_mu; [by []|exact: bigcupT_measurable|]. +apply: nondecreasing_cvg_measure; [by []|exact: bigcupT_measurable|]. move=> n m nm; apply/subsetPset; apply: setIS. by move/(nd_fleg c) : nm => /subsetPset. Unshelve. all: by end_near. Qed. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index 6803c75dc..ae0c1570d 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -69,7 +69,7 @@ Proof. move=> F ndF; rewrite /B /= => BF; split. by apply: bigcupT_measurable => n; have [] := BF n. have phiF x : phi (F i) x @[i \oo] --> phi (\bigcup_i F i) x. - rewrite /phi /= xsection_bigcup; apply: nondecreasing_cvg_mu. + rewrite /phi /= xsection_bigcup; apply: nondecreasing_cvg_measure. - by move=> n; apply: measurable_xsection; case: (BF n). - by apply: bigcupT_measurable => i; apply: measurable_xsection; case: (BF i). - by move=> m n mn; exact/subsetPset/le_xsection/subsetPset/ndF. @@ -89,7 +89,7 @@ Proof. move=> F ndF; rewrite /B /= => BF; split. by apply: bigcupT_measurable => n; have [] := BF n. have psiF x : psi (F i) x @[i \oo] --> psi (\bigcup_i F i) x. - rewrite /psi /= ysection_bigcup; apply: nondecreasing_cvg_mu. + rewrite /psi /= ysection_bigcup; apply: nondecreasing_cvg_measure. - by move=> n; apply: measurable_ysection; case: (BF n). - by apply: bigcupT_measurable => i; apply: measurable_ysection; case: (BF i). - by move=> m n mn; exact/subsetPset/le_ysection/subsetPset/ndF. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 4894aa3f3..8d55c854e 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -630,7 +630,7 @@ Let lebesgue_measure_itvoo_subr1 (a : R) : Proof. rewrite itv_bnd_open_bigcup//; transitivity (limn (lebesgue_measure \o (fun k => `]a - 1, a - k.+1%:R^-1]%classic : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. - by move=> ?; exact: measurable_itv. - by apply: bigcup_measurable => k _; exact: measurable_itv. - move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=]. @@ -728,7 +728,7 @@ Let lebesgue_measure_itv_bnd_infty x (a : R) : Proof. rewrite itv_bndy_bigcup_BRight; transitivity (limn (lebesgue_measure \o (fun k => [set` Interval (BSide x a) (BRight (a + k%:R))] : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. + by move=> k; exact: measurable_itv. + by apply: bigcup_measurable => k _; exact: measurable_itv. + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[->/=]. @@ -744,7 +744,7 @@ Let lebesgue_measure_itv_infty_bnd y (b : R) : Proof. rewrite itvNy_bnd_bigcup_BLeft; transitivity (limn (lebesgue_measure \o (fun k => [set` Interval (BLeft (b - k%:R)) (BSide y b)] : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_measure. + by move=> k; exact: measurable_itv. + by apply: bigcup_measurable => k _; exact: measurable_itv. + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->]. @@ -981,7 +981,7 @@ Proof. move=> mD Dfin epspos; pose Dn n := D `&` [set` `[-(n%:R), n%:R]]%R. have mDn n : measurable (Dn n) by exact: measurableI. have : mu \o Dn @ \oo --> mu (\bigcup_n Dn n). - apply: nondecreasing_cvg_mu => //. + apply: nondecreasing_cvg_measure => //. - by apply: bigcup_measurable => // ? _; exact: mDn. - move=> n m nm; apply/subsetPset; apply: setIS => z /=; rewrite !in_itv/=. move=> /andP[nz zn]; rewrite (le_trans _ nz)/= ?(le_trans zn) ?ler_nat//. @@ -1076,7 +1076,7 @@ rewrite leye_eq => /eqP /[dup] + ->. have {1}-> : D = \bigcup_n (F n `&` D) by rewrite -setI_bigcupl -RFU setTI. move=> FDp; apply/esym/eq_infty => M. have : (fun n => mu (F n `&` D)) @ \oo --> +oo. - rewrite -FDp; apply: nondecreasing_cvg_mu. + rewrite -FDp; apply: nondecreasing_cvg_measure. - by move=> i; apply: measurableI => //; exact: (ffin i).1. - by apply: bigcup_measurable => i _; exact: (measurableI _ _ (ffin i).1). - by move=> n m nm; apply/subsetPset; apply: setSI; exact/subsetPset/Fsub. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 002dcfe9e..94051429a 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -497,6 +497,35 @@ Qed. End rgenopens. End RGenOpens. +Module RGenOpenSets. +Section rgenopensets. +Variable R : realType. +Implicit Types a b : R. + +Definition G := @open R. + +Lemma open_ocitv_measurable (U : set R) : G U -> measurable U. +Proof. +move=> oU; rewrite (open_disjoint_itv_bigcup oU); +apply: sigma_algebra_bigcup => k. +have /is_intervalP -> := @open_disjoint_itv_is_interval _ U oU k. +exact : measurable_itv. +Qed. + +Lemma ocitv_open_measurable a b : <> `]a,b[%classic. +Proof. by apply: sub_sigma_algebra; rewrite/G. Qed. + +Lemma measuralbeE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split; [rewrite RGenOpens.measurableE|]; + apply: sigma_algebra_subl=> U. + rewrite/RGenOpens.G/= => [[a [b ->]]]; exact: ocitv_open_measurable. +by move=> /open_ocitv_measurable. +Qed. + +End rgenopensets. +End RGenOpenSets. + Section erealwithrays. Variable R : realType. Implicit Types (x y z : \bar R) (r s : R). @@ -1729,7 +1758,7 @@ have Ek0 k : \bigcap_n (E k n) = set0. have badn' k : exists n, mu (E k n) < ((eps / 2) / (2 ^ k.+1)%:R)%:E. pose ek : R := (eps / 2 / (2 ^ k.+1)%:R)%R. have : mu \o E k @ \oo --> mu set0. - rewrite -(Ek0 k); apply: nonincreasing_cvg_mu => //. + rewrite -(Ek0 k); apply: nonincreasing_cvg_measure => //. - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []]. - exact: bigcap_measurable. rewrite measure0; case/fine_cvg/(_ (interior (ball 0%R ek))). From 1da73bfed35bad4b4aabd26106805d38734bc647 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Thu, 2 Jul 2026 11:51:26 +0200 Subject: [PATCH 3/7] simplified lebesgue_display def --- theories/lebesgue_stieltjes_measure.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index c82beeb32..ef6c2c0e7 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -514,14 +514,15 @@ End wlength_extension. Arguments lebesgue_stieltjes_measure {R}. Definition measurableTypeR (R : realType) := - g_sigma_algebraType R.-ocitv.-measurable. + g_sigma_algebraType (@ocitv R). Section lebesgue_stieltjes_measure. Context {R : realType}. -Definition lebesgue_display : measure_display := (R.-ocitv.-measurable).-sigma. -Definition measurableR : set_system R := - (R.-ocitv.-measurable).-sigma.-measurable. +Definition lebesgue_display : measure_display := + (@ocitv R).-sigma. +Definition measurableR : set (set R) := + (@ocitv R).-sigma.-measurable. HB.instance Definition _ : Measurable lebesgue_display (measurableTypeR R) := Measurable.on (measurableTypeR R). From e9b90a99f0b23c3daac4976421e0648b4bf8eb52 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Thu, 2 Jul 2026 14:17:43 +0200 Subject: [PATCH 4/7] version without RGenOpenSets --- theories/measurable_realfun.v | 39 +++++------------------------------ 1 file changed, 5 insertions(+), 34 deletions(-) diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 94051429a..84355501c 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -93,10 +93,10 @@ Qed. End ps_infty. Section salgebra_ereal. -Variables (R : realType) (G : set_system R). -Let measurableR : set_system R := G.-sigma.-measurable. +Variables (R : realType) (G : set (set R)). +Let measurableR : set (set R) := G.-sigma.-measurable. -Definition emeasurable : set_system (\bar R) := +Definition emeasurable : set (set \bar R) := [set EFin @` A `|` B | A in measurableR & B in ps_infty]. Lemma emeasurable0 : emeasurable set0. @@ -418,7 +418,7 @@ Section rgencinfty. Variable R : realType. Implicit Types x y z : R. -Definition G : set_system R := [set A | exists x, A = `[x, +oo[%classic]. +Definition G : set (set R) := [set A | exists x, A = `[x, +oo[%classic]. Lemma measurable_itv_bnd_infty b x : G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. @@ -497,35 +497,6 @@ Qed. End rgenopens. End RGenOpens. -Module RGenOpenSets. -Section rgenopensets. -Variable R : realType. -Implicit Types a b : R. - -Definition G := @open R. - -Lemma open_ocitv_measurable (U : set R) : G U -> measurable U. -Proof. -move=> oU; rewrite (open_disjoint_itv_bigcup oU); -apply: sigma_algebra_bigcup => k. -have /is_intervalP -> := @open_disjoint_itv_is_interval _ U oU k. -exact : measurable_itv. -Qed. - -Lemma ocitv_open_measurable a b : <> `]a,b[%classic. -Proof. by apply: sub_sigma_algebra; rewrite/G. Qed. - -Lemma measuralbeE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. -Proof. -rewrite eqEsubset; split; [rewrite RGenOpens.measurableE|]; - apply: sigma_algebra_subl=> U. - rewrite/RGenOpens.G/= => [[a [b ->]]]; exact: ocitv_open_measurable. -by move=> /open_ocitv_measurable. -Qed. - -End rgenopensets. -End RGenOpenSets. - Section erealwithrays. Variable R : realType. Implicit Types (x y z : \bar R) (r s : R). @@ -1213,7 +1184,7 @@ Module NGenCInfty. Section ngencinfty. Implicit Types x y z : nat. -Definition G : set_system nat := [set A | exists x, A = `[x, +oo[%classic]. +Definition G : set (set nat) := [set A | exists x, A = `[x, +oo[%classic]. Lemma measurable_itv_bnd_infty b x : G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. From 039334fab9073024fd3953dee6fd7dd50c9634f5 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Thu, 2 Jul 2026 14:20:51 +0200 Subject: [PATCH 5/7] set_system instead of set (set _) --- theories/measurable_realfun.v | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 84355501c..5a0ae9734 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -93,10 +93,10 @@ Qed. End ps_infty. Section salgebra_ereal. -Variables (R : realType) (G : set (set R)). -Let measurableR : set (set R) := G.-sigma.-measurable. +Variables (R : realType) (G : set_system R). +Let measurableR : set_system R := G.-sigma.-measurable. -Definition emeasurable : set (set \bar R) := +Definition emeasurable : set_system \bar R := [set EFin @` A `|` B | A in measurableR & B in ps_infty]. Lemma emeasurable0 : emeasurable set0. @@ -418,7 +418,7 @@ Section rgencinfty. Variable R : realType. Implicit Types x y z : R. -Definition G : set (set R) := [set A | exists x, A = `[x, +oo[%classic]. +Definition G : set_system R := [set A | exists x, A = `[x, +oo[%classic]. Lemma measurable_itv_bnd_infty b x : G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. @@ -497,6 +497,7 @@ Qed. End rgenopens. End RGenOpens. + Section erealwithrays. Variable R : realType. Implicit Types (x y z : \bar R) (r s : R). @@ -1184,7 +1185,7 @@ Module NGenCInfty. Section ngencinfty. Implicit Types x y z : nat. -Definition G : set (set nat) := [set A | exists x, A = `[x, +oo[%classic]. +Definition G : set_system nat := [set A | exists x, A = `[x, +oo[%classic]. Lemma measurable_itv_bnd_infty b x : G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. From d53316cbaa0dfa33df2a3aabd789ca80c0e6139f Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 2 Jul 2026 21:49:35 +0900 Subject: [PATCH 6/7] Apply suggestion from @affeldt-aist --- theories/measurable_realfun.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 5a0ae9734..b48afd1de 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -96,7 +96,7 @@ Section salgebra_ereal. Variables (R : realType) (G : set_system R). Let measurableR : set_system R := G.-sigma.-measurable. -Definition emeasurable : set_system \bar R := +Definition emeasurable : set_system (\bar R) := [set EFin @` A `|` B | A in measurableR & B in ps_infty]. Lemma emeasurable0 : emeasurable set0. From 3228e8da31c6ed4921fdc2196e84fd5d1767bb30 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 3 Jul 2026 00:01:35 +0900 Subject: [PATCH 7/7] Apply suggestion from @affeldt-aist --- theories/measurable_realfun.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index b48afd1de..1fdbbb44f 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -496,8 +496,6 @@ Qed. End rgenopens. End RGenOpens. - - Section erealwithrays. Variable R : realType. Implicit Types (x y z : \bar R) (r s : R).