feat(Topology/Compactness/CompactSystem): introduce compact Systems by pfaffelh · Pull Request #25899 · leanprover-community/mathlib4

pfaffelh · 2025-06-15T11:45:51Z

A compact system is a set systems with the property that, whenever a countable intersections of sets in the set system is empty, there is a finite subset of sets with empty intersection. These are needed e.g. in measure theory if one wants to show sigma-additivity of a set function on a ring.

Main result: The set of sets which are either compact and closed, or univ, is a compact system.
Introduce Dissipate s x := ⋂ y ≤ x, s y (Data/Set/Dissipate), which is parallel to Data/Set/Accumulate.

Co-authored-by: Rémy Degenne remydegenne@gmail.com

This PR continues the work from #24541.

Original PR: #24541

github-actions · 2025-06-15T11:46:59Z

PR summary 39aeb68534

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Data.Set.Dissipate` (new file)	620
`Mathlib.Topology.Compactness.CompactSystem` (new file)	726

Declarations diff

+ IsCompactSystem
+ IsPiSystem.dissipate_mem
+ IsPiSystem.iff_of_empty_mem
+ antitone_dissipate
+ directed_dissipate
+ dissipate
+ dissipate_bot
+ dissipate_def
+ dissipate_dissipate
+ dissipate_eq
+ dissipate_eq_empty
+ dissipate_subset
+ dissipate_subset_dissipate
+ dissipate_succ
+ dissipate_zero
+ exists_dissipate_eq_empty_iff
+ exists_dissipate_eq_empty_iff_of_directed
+ exists_subset_dissipate_of_directed
+ finite_of_empty
+ iInter_dissipate
+ iInter_subset_dissipate
+ iff_directed
+ iff_directed'
+ iff_isCompactSystem_of_or_empty
+ iff_isCompactSystem_of_or_univ
+ iff_nonempty_iInter
+ iff_nonempty_iInter_of_lt
+ mem_dissipate
+ mono
+ of_IsEmpty
+ of_isCompact
+ of_isCompact_isClosed
+ of_isCompact_isClosed_or_univ

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

sgouezel · 2025-07-26T14:37:49Z

+open Nat
+
+@[simp]
+theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :


if you want to use dissipate in the lemma name, it should also appear in the statement.

Can you also use it on the left hand side?

I will open a new PR with only the changes in Dissipate.lean as asked for below. My answers here apply to the new PR.
The new PR is here:
#33975

Now it is also on the left hand side.

pfaffelh · 2025-08-20T20:22:37Z

-awaiting-author

sgouezel

Could you maybe split off the dissipate part to another PR? It's much easier to review two 200 lines PR that one 400 lines, because of available time slots.

sgouezel · 2025-09-18T19:54:45Z

+def dissipate [LE α] (s : α → Set β) (x : α) : Set β :=
+  ⋂ y ≤ x, s y
+
+@[simp]


This shouldn't be @[simp]. Otherwise, there's no point in introducing the definition if you want to remove it whenever it is used.

Ok, this makes a lot of sense.

sgouezel · 2025-09-18T19:55:36Z

+theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by
+  simp only [dissipate_def, mem_iInter]
+
+theorem dissipate_subset [Preorder α] {x y : α} (hy : y ≤ x) : dissipate s x ⊆ s y :=


Wouldn't [LE α] suffice here?

Yes, it does. Changed.

sgouezel · 2025-09-18T19:56:00Z

+theorem dissipate_subset [Preorder α] {x y : α} (hy : y ≤ x) : dissipate s x ⊆ s y :=
+  biInter_subset_of_mem hy
+
+theorem iInter_subset_dissipate [Preorder α] (x : α) : ⋂ i, s i ⊆ dissipate s x := by


sgouezel · 2025-09-18T19:56:39Z

+  antitone_dissipate h
+
+@[simp]
+theorem dissipate_dissipate [Preorder α] {s : α → Set β} {x : α} :


if a lemma name contains dissipate, the statement should also contain dissipate.

True, changed. (Since I had dissipate_def as simp before, I used the normal form in the lemma to start with.)

sgouezel · 2025-09-18T19:56:48Z

+    exact fun i hi z hz ↦ biInter_subset_of_mem <| le_trans hz hi
+
+@[simp]
+theorem iInter_dissipate [Preorder α] : ⋂ x, ⋂ y, ⋂ (_ : y ≤ x), s y = ⋂ x, s x := by


sgouezel · 2025-09-18T20:00:44Z

+lemma dissipate_zero (s : ℕ → Set β) : dissipate s 0 = s 0 := by
+  simp [dissipate_def]
+
+lemma exists_subset_dissipate_of_directed {s : ℕ → Set α}


Can you add a docstring explaining the content of the lemma?

sgouezel · 2025-09-18T20:02:41Z

+
+lemma directed_dissipate {s : ℕ → Set α} :
+    Directed (fun (x y : Set α) => y ⊆ x) (dissipate s) :=
+     antitone_dissipate.directed_ge


Suggested change

antitone_dissipate.directed_ge

antitone_dissipate.directed_ge

sgouezel · 2025-09-18T20:03:37Z

+
+lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α)
+    (hd : Directed (fun (x y : Set α) => y ⊆ x) C) :
+    (∃ n, C n = ∅) ↔ (∃ n, dissipate C n = ∅) := by


Could you exchange the two sides of the iff, to match the lemma statement? In general, the more complicated term in an iff is put to its left, because rw or simp operate from left to right.

Thanks, done.

sgouezel · 2025-09-18T20:04:19Z

+`p (dissipate s n)` holds. -/
+lemma IsPiSystem.dissipate_mem {s : ℕ → Set α} {p : Set (Set α)}
+    (hp : IsPiSystem p) (h : ∀ n, s n ∈ p) (n : ℕ) (h' : (dissipate s n).Nonempty) :
+      (dissipate s n) ∈ p := by


Suggested change

(dissipate s n) ∈ p := by

dissipate s n ∈ p := by

sgouezel · 2025-09-18T20:05:00Z

+    exact Set.Nonempty.mono hm (h m)
+
+/-- For a ∩-stable set of sets `p` on `α` and a sequence of sets `s` with this attribute,
+`p (dissipate s n)` holds. -/


Suggested change

`p (dissipate s n)` holds. -/

`dissipate s n` belongs to `p`. -/

(The lemma is about a set of sets, not sets with some property)

mathlib4-merge-conflict-bot · 2025-11-19T07:46:19Z

This pull request has conflicts, please merge master and resolve them.

…l faithfulness of `toDescentData` (leanprover-community#33179) We show that a pseudofunctor `F` is a prestack iff the functors `F.toDescentData f` are fully faithful whenever `f` is a covering family. We also introduce predicates `F.IsPrestackFor R` and `F.IsStackFor R` (for a presieve `R`) saying the corresponding functor `F.DescentData (fun (f : R.category) ↦ f.obj.hom)` is fully faithful or an equivalence.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

… subgraphs (leanprover-community#32043) We characterise subgraphs `H ≤ G` which are maximal among acyclic subgraphs of `G` as those for which `H.Reachable = G.Reachable`. We also prove that if `x` and `y` are not reachable in `G`, then `G ⊔ fromEdgeSet {s(x,y)}` is acyclic iff `G` is. Co-authored-by: twwar <tom.waring@unimelb.edu.au>

…eanprover-community#33341) Now that `range` and `ker` take in a `LinearMap` instead of a `LinearMapClass`, these lemmas are the same thing as the linear map versions.

…td.Symm` (leanprover-community#33325)

…1332) We define an exponentiable morphism `f : I ⟶ J` to be a morphism with a chosen pullback functor `Over J ⥤ Over I` together with a right adjoint, called the pushforward functor. We use this PR in the PR branch `lccc-basic`. ```mermaid graph TD A[ChosenPullbacksAlong.lean] --> A'[Over.lean] A' --> B[Sections.lean] A --> C[ExponentiableMorphism.lean] B --> D[Basic.lean] C --> D D --> E[Types.lean] E --> F[Presheaves.lean] D --> G[Beck-Chevalley.lean] %% Define highlight style classDef highlight fill:#ffe599,stroke:#d4a017,stroke-width:2px; %% Apply to one node class C highlight; ``` Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

…eanprover-community#33301)

…er-community#33422) Some important maps (e.g., `Complex.exp` or `x ↦ x ^ n`) aren't covering maps over the whole space.

…#33371)

…-community#33459) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Fix incorrect comments

In this PR, we define stacks using the language of pseudo-functors `F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat`. If `J` is a Grothendieck topology on `C`, we say that `F` is a stack if it is a prestack (i.e. descent of morphisms holds) if the descent is effective. This means that the functor `F.obj (.mk (op S))` to the category of descent data relative to a covering of `S` is essentially surjective. As the prestack condition already implies that these functors are fully faithful, this means that these functors are equivalences of categories. Co-authored-by: Christian Merten [christian@merten.dev](mailto:christian@merten.dev)

…nprover-community#33468)

…eanprover-community#33783) leanprover-community#33696 changed the linting step so that it pipes its output into `tee`; this causes `lake exe runLinter` to block buffer its output, which means that if the linters freeze (cf. [#mathlib4 > slow linting step CI?](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/slow.20linting.20step.20CI.3F/with/567049377)), we may not see all of the log output. This PR uses [`stdbuf -oL`](https://www.gnu.org/software/coreutils/manual/html_node/stdbuf-invocation.html) to make the output line buffered instead, which should solve this.

Update some stale file references.

…ty#33626) This adds some API for upper hemicontinuous functions, including their behavior under pointwise union or intersection, post-composition by the preimage of a closed embedding (actually, injectivity is not necessary), and the characterization in terms of the convergence of sequences. This is is useful for a forthcoming PR proving the upper hemicontinuity of the spectrum in Banach algebras. Analogous results of lower hemicontinuous functions are *not* included because they are not as easily obtained from their upper counterparts as is the case for upper/lower semicontinuity, and our downstream applications involve upper hemicontinuity alone. - [ ] depends on: leanprover-community#33623 - [ ] depends on: leanprover-community#33624 - [ ] depends on: leanprover-community#33625

…mmunity#33524) The old names have been deprecated and removed from the codebase, but the docstring still refers to them.

…mmunity#33216) Adds a new file with facts about algebra representations. Proves Schur's lemma (any endomorphism of an algebra representation over an algebraically closed field is scalar) and proves that every finite-dimensional representation of a commutative algebra over an algebraically closed field is one-dimensional. Co-authored-by: Stepan <stepurik@stanford.edu>

…prover-community#32163) The interval integral c..x is absolutely continuous wrt x. Part of originally planned leanprover-community#29508

Found by extending the `whitespace` style linter to proof bodies of structures/instances in leanprover-community#33393.

…td.Refl` (leanprover-community#33755)

…prover-community#31960)

…munity#33562) This PR proves the three `proof_wanted` statements for `convexComboPair`: - `convexComboPair_zero`: weight 0 on first point gives the second point - `convexComboPair_one`: weight 1 on first point gives the first point - `convexComboPair_same`: any convex combo of a point with itself is that point Also adds supporting lemmas: - `StdSimplex.ext`: extensionality lemma for `StdSimplex` - `StdSimplex.mk_single`: simp lemma for constructor applied to single - `@[simp]` attribute on `ConvexSpace.single` 🤖 Prepared with Claude Code

…er-community#33603) `to_additive` has some troublesome interactions with the module system, because it sometimes relies on unfolding theorems whose value is not exported. This PR fixes that by never unfolding these theorems, and instead creating their translation the first time they appear. This will help remove some instances of `import all` and instances of `proofsInPublic`. The only theorems that we still unfold are the auxiliary theorems created by `simp`. These have very small proofs, and these proofs are always exported, so it is fine to unfold them.

…unity#30799) One version is about torsion-free monoids, the other one about linearly ordered monoids. I argue that all linearly ordered monoids of interest are torsion-free, and therefore the correct lemma to keep is the former. As a byproduct, I must move a few `MonoidHom` lemmas. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Should.20linear.20ordered.20comm.20monoids.20with.20zero.20be.20torsion-free)

…munity#33308) add the following helpers: - IsNowhereDense.isMeagre - isMeagre_biUnion - exists_of_not_meagre_biUnion - Topology.IsInducing.isMeagre_image - IsMeagre.image_val This PR follows leanprover-community#32740, which adds helpers for IsNowhereDense. These lemmas will help to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441).

…um (leanprover-community#32238) From ProofBench

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

…eanprover-community#28742) cf. leanprover-community#28324 (comment)

…3975) Introduce Dissipate s x := ⋂ y ≤ x, s y (Data/Set/Dissipate), which is parallel to Data/Set/Accumulate and provide some API for it. This will be used for compact systems in another PR. This PR continues the work from #25899. Co-authored-by: pfaffelh <p.p@stochastik.uni-freiburg.de>

…3975) Introduce Dissipate s x := ⋂ y ≤ x, s y (Data/Set/Dissipate), which is parallel to Data/Set/Accumulate and provide some API for it. This will be used for compact systems in another PR. This PR continues the work from #25899. Co-authored-by: pfaffelh <p.p@stochastik.uni-freiburg.de> Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

…anprover-community#33975) Introduce Dissipate s x := ⋂ y ≤ x, s y (Data/Set/Dissipate), which is parallel to Data/Set/Accumulate and provide some API for it. This will be used for compact systems in another PR. This PR continues the work from leanprover-community#25899. Co-authored-by: pfaffelh <p.p@stochastik.uni-freiburg.de> Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

This was referenced Jun 15, 2025

feat(Topology/Compactness/CompactSystem): set system of finite unions of sets in a compact system is again a compact system #25900

Closed

feat(Topology/Compactness/CompactSystem): closed and compact square cylinders form a compact system #25906

Closed

RemyDegenne mentioned this pull request Jul 12, 2025

feat(Topology/Compactness/CompactSystem): introduce compact Systems #24541

Closed

RemyDegenne added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jul 12, 2025

sgouezel reviewed Jul 26, 2025

View reviewed changes

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 26, 2025

pfaffelh force-pushed the pfaffelh_compactSystem branch from 36c0630 to e94c743 Compare August 19, 2025 20:21

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 20, 2025

leanprover-community-bot-assistant assigned PatrickMassot Aug 31, 2025

sgouezel reviewed Sep 18, 2025

View reviewed changes

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 19, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

RemyDegenne added the brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals label Nov 23, 2025

joelriou and others added 14 commits January 9, 2026 23:18

feat: cardinality of Hahn series inverse (leanprover-community#32643)

2c67626

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

feat: stdPart x = sSup {r | r < x} (leanprover-community#33007)

e8634b0

chore(Topology/Algebra/Module/LinearMap): deprecate duplicate lemmas (l…

1b6ed25

…eanprover-community#33341) Now that `range` and `ker` take in a `LinearMap` instead of a `LinearMapClass`, these lemmas are the same thing as the linear map versions.

chore(Order/Defs/Unbundled): deprecate IsSymm in favor of core's `S…

616962e

…td.Symm` (leanprover-community#33325)

chore(Algebra/Central/End): generalize Algebra.IsCentral.instEnd (l…

0411b42

…eanprover-community#33301)

feat(Homotopy/Lifting): add a lemma about IsCoveringMapOn (leanprov…

9334a88

…er-community#33422) Some important maps (e.g., `Complex.exp` or `x ↦ x ^ n`) aren't covering maps over the whole space.

feat(Probability): Right continuous filtrations (leanprover-community…

df12474

…#33371)

feat: FTaylorSeries of the composition with an affine map (leanprover…

bb09d6f

…-community#33459) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

chore: Fix Dihedral comments (leanprover-community#33483)

314af9a

Fix incorrect comments

feat(RingTheory): polynomial is integral <-> coeffs are integral (lea…

b9694a5

…nprover-community#33468)

bryangingechen and others added 16 commits January 9, 2026 23:18

doc(Algebra): fix file refs (leanprover-community#33620)

8b9c027

Update some stale file references.

fix: Rename constructors in Irrational.lean docstrings (leanprover-co…

87a4616

…mmunity#33524) The old names have been deprecated and removed from the codebase, but the docstring still refers to them.

feat(MeasureTheory): interval integral is absolutely continuous (lean…

d5a2b31

…prover-community#32163) The interval integral c..x is absolutely continuous wrt x. Part of originally planned leanprover-community#29508

chore: fix whitespace (leanprover-community#33747)

601c22f

Found by extending the `whitespace` style linter to proof bodies of structures/instances in leanprover-community#33393.

chore(Order/Defs/Unbundled): deprecate IsRefl in favor of core's `S…

b6e3de2

…td.Refl` (leanprover-community#33755)

feat: a lower bound for the volume of a cone on the unit sphere (lean…

bbcc617

…prover-community#31960)

feat(Combinatorics/SimpleGraph): distributivity of box product over s…

3566c35

…um (leanprover-community#32238) From ProofBench

cs0

aebf7c4

Update Mathlib.lean

2a48ffd

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

pfaffelh mentioned this pull request Jan 14, 2026

[Merged by Bors] - feat(Data/Set/Dissipate): Introduce dissipate s x := ⋂ y ≤ x, s y #33975

Closed

bryangingechen and others added 2 commits January 17, 2026 10:20

chore: clean up porting note left after leanprover-community#28324 (l…

9125043

…eanprover-community#28742) cf. leanprover-community#28324 (comment)

doc: fix repeated typo "nonegative" (leanprover-community#29637)

9b337fd

pfaffelh mentioned this pull request Mar 2, 2026

[Merged by Bors] - feat(Topology/Compactness/CompactSystem): introduce compact Systems #36013

Closed

pfaffelh closed this Mar 2, 2026

	antitone_dissipate.directed_ge
	antitone_dissipate.directed_ge

	`p (dissipate s n)` holds. -/
	`dissipate s n` belongs to `p`. -/

Conversation

pfaffelh commented Jun 15, 2025

Uh oh!

github-actions Bot commented Jun 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 39aeb68534

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pfaffelh Jan 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

pfaffelh commented Aug 20, 2025

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

20 participants

github-actions Bot commented Jun 15, 2025 •

edited

Loading

pfaffelh Jan 14, 2026 •

edited

Loading