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

[pfaffelh]

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: [Merged by Bors] - chore: fix more odd indentation #24906
• depends on: feat(Topology/Compactness/CompactSystem): introduce compact Systems #25899

---

This PR continues the work from #24543.

Original PR: #24543

[github-actions]

PR summary 39aeb68534

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Constructions.Cylinders	765	770	+5 (+0.65%)

Import changes for all files

Files	Import difference
30 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.FiniteDimensionalLaws Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Stopping	2
Mathlib.MeasureTheory.Constructions.Cylinders	5
Mathlib.Data.Set.Dissipate (new file)	620
Mathlib.Topology.Compactness.CompactSystem (new file)	816

---

Declarations diff

+ Fin.elim0'.{u}
+ IsCompactSystem
+ IsCompactSystem.compactClosedOrUnivPi
+ IsCompactSystem.compactClosedPi
+ IsPiSystem.dissipate_mem
+ IsPiSystem.iff_of_empty_mem
+ MeasureTheory.compactClosedSquareCylinders
+ Nat.prefixInduction
+ Nat.prefixInduction'
+ Nat.prefixInduction'_spec
+ Nat.prefixInduction.aux
+ Nat.prefixInduction.auxConsistent
+ Nat.prefixInduction_spec
+ antitone_dissipate
+ biInter_univ_pi_empty_iff
+ 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_le_mem_measurableCylinders
+ iInter_pi_empty_iff
+ iInter_subset_dissipate
+ 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
+ mono
+ 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_eq_iUnion_image'
+ squareCylinders_subset_of_or_univ
+ 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).

[leanprover-community-bot-assistant]

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

[mathlib4-merge-conflict-bot]

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - chore: fix more odd indentation #24906
• feat(Topology/Compactness/CompactSystem): introduce compact Systems #25899
  By Dependent Issues (🤖). Happy coding!