feat (Topology/Compactness/CompactSystem): Set system of finite unions of sets in a compact system is again a compact system by pfaffelh · Pull Request #24543 · leanprover-community/mathlib4

pfaffelh · 2025-05-02T07:16:14Z

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

A compact system is a set system with the following property: If all finite intersections of a sequence in the set system is non-empty, the countable intersection is not empty.

Starting with a compact system, consider the finite unions of sets in the copact system. Such sets again form a compact system (IsCompactSystem.union.isCompactSystem).

depends on: feat(Topology/Compactness/CompactSystem): introduce compact Systems #24541
depends on: feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a compact system. #24542

github-actions · 2025-05-02T07:17:18Z

PR summary 3bb3ee2af4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
29 files `Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders` `Mathlib.MeasureTheory.Constructions.Projective` `Mathlib.MeasureTheory.Function.FactorsThrough` `Mathlib.Probability.BorelCantelli` `Mathlib.Probability.Independence.Conditional` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Probability.Kernel.CompProdEqIff` `Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Probability.Kernel.Condexp` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.Probability.Kernel.Posterior` `Mathlib.Probability.Kernel.RadonNikodym` `Mathlib.Probability.Martingale.Basic` `Mathlib.Probability.Martingale.BorelCantelli` `Mathlib.Probability.Martingale.Centering` `Mathlib.Probability.Martingale.Convergence` `Mathlib.Probability.Martingale.OptionalSampling` `Mathlib.Probability.Martingale.OptionalStopping` `Mathlib.Probability.Martingale.Upcrossing` `Mathlib.Probability.Moments.SubGaussian` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Process.Filtration` `Mathlib.Probability.Process.HittingTime` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Process.Stopping`	2
`Mathlib.MeasureTheory.Constructions.Cylinders`	5
`Mathlib.Data.Set.Dissipate` (new file)	609
`Mathlib.Topology.Compactness.CompactSystem` (new file)	801

Declarations diff

+ Dissipate
+ Fin.elim0'.{u}
+ IsCompactSystem
+ IsCompactSystem.compactClosedPi
+ IsPiSystem.iff_of_empty_mem
+ MeasureTheory.compactClosedSquareCylinders
+ Nat.prefixInduction
+ Nat.prefixInduction'
+ Nat.prefixInduction'_spec
+ Nat.prefixInduction.aux
+ Nat.prefixInduction.auxConsistent
+ Nat.prefixInduction_spec
+ biInter_dissipate
+ biInter_univ_pi_empty_iff
+ directed_dissipate
+ dissipate_antitone
+ dissipate_bot
+ dissipate_def
+ dissipate_eq
+ dissipate_eq_empty
+ dissipate_of_piSystem
+ dissipate_subset
+ dissipate_subset_dissipate
+ dissipate_subset_iInter
+ 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_le_mem_measurableCylinders
+ iInter_pi_empty_iff
+ iInter_univ_pi_empty_iff
+ iUnion_le_mem_measurableCylinders
+ iff_directed
+ iff_directed'
+ iff_isCompactSystem_of_or_empty
+ iff_isCompactSystem_of_or_univ
+ iff_nonempty_iInter
+ iff_nonempty_iInter_of_lt
+ iff_nonempty_iInter_of_lt'
+ inter_sUnion_eq_empty
+ isCompactSystem.compactClosedSquareCylinders
+ k
+ l1
+ mem_dissipate
+ mem_of_union
+ mem_of_union.spec
+ mem_squareCylinders
+ mono
+ nonempty_isCompactIsClosed
+ of_IsEmpty
+ of_isCompact
+ of_isCompact_isClosed
+ of_isCompact_isClosed_or_univ
+ pi
+ pi_antitone
+ pi_image_eq_of_subset
+ pi_nonempty_iff'
+ q
+ q_iff_iInter
+ q_iff_iInter'
+ sInter_memOfUnion_isSubset
+ sInter_memOfUnion_nonempty
+ squareCylinder
+ squareCylinders
+ squareCylinders_eq_iUnion_image'
+ squareCylinders_subset_pi
+ step'
+ step0
+ step_of
+ union
+ union.isCompactSystem
+ union.mem_iff

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).

mathlib4-dependent-issues-bot · 2025-05-02T07:46:45Z

This PR/issue depends on:

feat(Topology/Compactness/CompactSystem): introduce compact Systems #24541
feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a compact system. #24542
By Dependent Issues (🤖). Happy coding!

leanprover-community-bot-assistant · 2025-05-02T21:25:57Z

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

leanprover-community-bot-assistant · 2025-05-27T15:54:03Z

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

nomeata

Some docstring suggestions, without any ambition at completeness :-)

nomeata · 2025-06-10T22:30:45Z

Mathlib/Topology/Compactness/CompactSystem.lean

+    ∀ n (k : (i : Fin n) → (β i)) (_ : q n k),
+    { a : β n // q (n+1) (Fin.snoc k a)})
+
+/-- In this section, we prove a general induction principle, which we need for the construction


Probably this should be a module doc string, not a declaration doc string?

Suggested change

/-- In this section, we prove a general induction principle, which we need for the construction

/-! In this section, we prove a general induction principle, which we need for the construction

nomeata · 2025-06-10T22:31:59Z

Mathlib/Topology/Compactness/CompactSystem.lean

+`(n : ℕ) : β n` constructs the next element satisfying `q (n + 1) _` from a proof of `q n k`
+and finding the next element.
+
+In comparisong to other induction principles, the proofs of `q n k` are needed in order to find


Suggested change

In comparisong to other induction principles, the proofs of `q n k` are needed in order to find

In comparison to other induction principles, the proofs of `q n k` are needed in order to find

nomeata · 2025-06-10T22:32:34Z

Mathlib/Topology/Compactness/CompactSystem.lean

+/- An auxiliary definition for `Nat.prefixInduction`. -/
+def Nat.prefixInduction.aux : ∀ (n : Nat), { k : (i : Fin n) → (β i) // q n k }


Suggested change

/- An auxiliary definition for `Nat.prefixInduction`. -/

def Nat.prefixInduction.aux : ∀ (n : Nat), { k : (i : Fin n) → (β i) // q n k }

/- An auxiliary definition for `Nat.prefixInduction`:

The `n`’th prefix of the sequence constructed by `Nat.prefixInduction`. -/

def Nat.prefixInduction.aux : ∀ (n : Nat), { k : (i : Fin n) → (β i) // q n k }

nomeata · 2025-06-10T22:33:45Z

Mathlib/Topology/Compactness/CompactSystem.lean

+      let ⟨a, ha⟩ := step n k hk
+      ⟨Fin.snoc k a, ha⟩
+
+theorem Nat.prefixInduction.auxConsistent :


Suggested change

theorem Nat.prefixInduction.auxConsistent :

/-- The `i`th elements of any prefix constructed by `aux` (with at least `i` elements) are the same. -/

theorem Nat.prefixInduction.auxConsistent :

RemyDegenne · 2025-07-12T07:03:30Z

Closing: replaced by #25900

pfaffelh and others added 17 commits March 23, 2025 17:48

not finished with compactUnion

c91a05c

small progress

d96cc41

improve

4e17015

transfer

3223369

finished zero case

9500281

transfer2

35471a0

deleted several examples

a94940d

almost...

7f5fa3c

main works

94a15f4

define union

da9677f

progress

8de478e

no problems anymore

f546b8c

resolved merge conflict with master

6ddc847

typos

bd58de9

merged ...2

5cc9713

typo

ab419da

deleted copy

b5132d1

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 2, 2025

typo

24784c7

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 2, 2025

Merge branch 'pfaffelh_compactSystem2' into pfaffelh_compactSystem3

07ceefc

pfaffelh changed the title ~~feat (Topology/Compactness/CompactSystem): Set set system of finite unions of sets in a compact system is again a compact system~~ feat (Topology/Compactness/CompactSystem): Set system of finite unions of sets in a compact system is again a compact system May 2, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 2, 2025

pfaffelh added 3 commits May 3, 2025 07:13

added Nat

8c62e57

merge 2

aaeb552

added docstring union

eda3dc3

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 3, 2025

grunweg added the t-topology Topological spaces, uniform spaces, metric spaces, filters label May 3, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 27, 2025

pfaffelh added 2 commits May 28, 2025 22:11

added prefixINduction

2fdbceb

halfway

9c42352

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 30, 2025

Merge branch 'pfaffelh_compactSystem2' into pfaffelh_compactSystem3

57f68ff

github-actions 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 May 30, 2025

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 30, 2025

runs half

661d016

github-actions 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 Jun 1, 2025

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 1, 2025

reworked recursion

7c7f263

github-actions 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 Jun 9, 2025

pfaffelh added 2 commits June 9, 2025 23:00

Merge branch 'pfaffelh_compactSystem2' into pfaffelh_compactSystem3

31bc1ef

fix namespaces

cc83bfd

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 9, 2025

pfaffelh added 3 commits June 9, 2025 23:32

no errors

794929c

no errors2

64acd7c

no errors3

9fe564c

nomeata reviewed Jun 10, 2025

View reviewed changes

pfaffelh mentioned this pull request 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

2 tasks

RemyDegenne closed this Jul 12, 2025

YaelDillies deleted the pfaffelh_compactSystem3 branch August 18, 2025 07:33

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

feat (Topology/Compactness/CompactSystem): Set system of finite unions of sets in a compact system is again a compact system#24543
pfaffelh wants to merge 32 commits intopfaffelh_compactSystem2from
pfaffelh_compactSystem3

pfaffelh commented May 2, 2025 •

edited

Loading

Uh oh!

github-actions bot commented May 2, 2025 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented May 2, 2025

Uh oh!

leanprover-community-bot-assistant commented May 2, 2025

Uh oh!

leanprover-community-bot-assistant commented May 27, 2025

Uh oh!

nomeata left a comment

Uh oh!

nomeata Jun 10, 2025

Uh oh!

nomeata Jun 10, 2025

Uh oh!

nomeata Jun 10, 2025

Uh oh!

nomeata Jun 10, 2025

Uh oh!

RemyDegenne commented Jul 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

	/-- In this section, we prove a general induction principle, which we need for the construction
	/-! In this section, we prove a general induction principle, which we need for the construction

	In comparisong to other induction principles, the proofs of `q n k` are needed in order to find
	In comparison to other induction principles, the proofs of `q n k` are needed in order to find

		/- An auxiliary definition for `Nat.prefixInduction`. -/
		def Nat.prefixInduction.aux : ∀ (n : Nat), { k : (i : Fin n) → (β i) // q n k }

	theorem Nat.prefixInduction.auxConsistent :
	/-- The `i`th elements of any prefix constructed by `aux` (with at least `i` elements) are the same. -/
	theorem Nat.prefixInduction.auxConsistent :

Conversation

pfaffelh commented May 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented May 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3bb3ee2af4

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented May 2, 2025

Uh oh!

leanprover-community-bot-assistant commented May 2, 2025

Uh oh!

leanprover-community-bot-assistant commented May 27, 2025

Uh oh!

nomeata left a comment

Choose a reason for hiding this comment

Uh oh!

nomeata Jun 10, 2025

Choose a reason for hiding this comment

Uh oh!

nomeata Jun 10, 2025

Choose a reason for hiding this comment

Uh oh!

nomeata Jun 10, 2025

Choose a reason for hiding this comment

Uh oh!

nomeata Jun 10, 2025

Choose a reason for hiding this comment

Uh oh!

RemyDegenne commented Jul 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

pfaffelh commented May 2, 2025 •

edited

Loading

github-actions bot commented May 2, 2025 •

edited

Loading