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

[pfaffelh]

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

This was previously #25900.

---

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

[github-actions]

PR summary 028964f2c6

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Compactness.CompactSystem	706	709	+3 (+0.42%)

Import changes for all files

Files	Import difference
Mathlib.Topology.Compactness.CompactSystem	3

---

Declarations diff

+ Nat.prefixInduction
+ Nat.prefixInduction'
+ Nat.prefixInduction'_spec
+ Nat.prefixInduction.aux
+ Nat.prefixInduction.auxConsistent
+ Nat.prefixInduction_spec
+ dissipate_eq_ofFin
+ iff_nonempty_iInter_of_lt'
+ inter_sUnion_eq_empty
+ isCompactSystem_supClosure_insert_empty
+ memOfUnion
+ memOfUnion.spec
+ mem_subClosure_insert_empty_iff
+ mem_subClosure_set_iff
+ q
+ q_iff_iInter
+ q_snoc_iff_iInter
+ sInter_memOfUnion_isSubset
+ sInter_memOfUnion_nonempty
+ step'
+ step0

You can run this locally as follows

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

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

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

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(Topology/Compactness/CompactSystem): introduce compact Systems #36013
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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