From 35c4d19e4b5beb3f6e1f64331f72e32c5494405d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 9 Oct 2026 10:45:51 +0900 Subject: [PATCH] generalization observed in another PR Co-authored-by: Lionel Blatter --- CHANGELOG_UNRELEASED.md | 3 +++ theories/esum.v | 8 ++++---- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 20a0c70f10..f6367063d1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -136,6 +136,9 @@ + lemmas `within_continuousD`, `within_continuousB`, `within_continuousN` + lemmas `le_closed_ball`, `closed_ball0` +- in `esum.v`: + + lemmas `esum_bigcupT`, `esum_bigcup` + ### Deprecated - in `pseudometric_normed_Zmodule.v`: diff --git a/theories/esum.v b/theories/esum.v index a6a94193b1..97e21ab519 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -776,8 +776,8 @@ Qed. Arguments esum_set_image {R T} a e P. Section esum_bigcup. -Context {R : realType} {T : choiceType} (K : set nat). -Implicit Types (J : nat -> set T) (a : T -> \bar R). +Context {R : realType} {T U : choiceType} (K : set U). +Implicit Types (J : U -> set T) (a : T -> \bar R). Lemma esum_bigcupT J a : trivIset setT J -> (forall x, 0 <= a x) -> \esum_(i in \bigcup_(k in K) (J k)) a i = @@ -824,8 +824,8 @@ Qed. End esum_bigcup. -Arguments esum_bigcupT {R T K} J a. -Arguments esum_bigcup {R T K} J a. +Arguments esum_bigcupT {R T U K} J a. +Arguments esum_bigcup {R T U K} J a. Lemma nneseries_sum_bigcup {R : realType} (T : choiceType) (F : (set T)^nat) (f : T -> \bar R) : trivIset [set: nat] F -> (forall i, 0 <= f i)%E ->