feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a compact system.

[pfaffelh]

feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a
compact system.

A square cylinder is a set of the form s.pi t in a product space. A closed compact square cylinder has IsClosed (t i) and IsCompact (t i) for all i ∈ s. This set system is a compact system (as introduced in PR #24541).

Streamline the definition of square cylinders in MeasureTheory/Constructions/Cylinders on the way.

Co-authors: Rémy Degenne remy.degenne@inria.fr

---

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

[github-actions]

PR summary 3bb3ee2af4

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Constructions.Cylinders	745	750	+5 (+0.67%)

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
+ IsCompactSystem
+ IsCompactSystem.compactClosedPi
+ IsPiSystem.iff_of_empty_mem
+ MeasureTheory.compactClosedSquareCylinders
+ 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
+ isCompactSystem.compactClosedSquareCylinders
+ mem_dissipate
+ 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'
+ squareCylinder
+ squareCylinders
+ squareCylinders_eq_iUnion_image'
+ squareCylinders_subset_pi

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]

This PR/issue depends on:

• feat(Topology/Compactness/CompactSystem): introduce compact Systems #24541
  By Dependent Issues (🤖). Happy coding!

[leanprover-community-bot-assistant]

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

[leanprover-community-bot-assistant]

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

[RemyDegenne]

I'm closing this PR because it has been replaced by #25906