feat(Topology/Compactness/CompactSystem): set system of countable intersections 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 countable intersections of sets in the copact system. Such sets again form a compact system.

---

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

[github-actions]

PR summary 034c50cbf6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Probability.Independence.Process	-1673
Mathlib.Probability.Independence.Process.Basic	1673
Mathlib.Probability.Independence.Process.HasIndepIncrements	2103
Mathlib.NumberTheory.RatFunc.Ostrowski	2222

---

Declarations diff

+ HasIndepIncrements
+ HasIndepIncrements.indepFun_eval_sub
+ HasIndepIncrements.indepFun_sub_sub
+ HasIndepIncrements.map
+ HasIndepIncrements.map'
+ HasIndepIncrements.nat
+ HasIndepIncrements.neg
+ HasIndepIncrements.of_nat
+ HasIndepIncrements.smul
+ Ioi_diff_Ioc
+ adicValuation_ne_inftyValuation
+ adicValuation_not_isEquiv_infty_valuation
+ coePolynomial_eq_algebraMap
+ continuousOn_Ici_primitive_Ici
+ continuousOn_Ici_primitive_Ioi
+ continuousOn_Iic_primitive_Iic
+ continuousOn_Iic_primitive_Iio
+ continuousWithinAt_Ici_primitive_Ioi
+ continuousWithinAt_Iic_primitive_Iio
+ exists_zpow_uniformizingPolynomial
+ hasIndepIncrements_iff_nat
+ instance : Valuation.IsTrivialOn Fq (inftyValuation Fq)
+ intDegree_div
+ integral_Ico_eq_integral_Ioc
+ integral_Iio_sub_Iio
+ integral_Iio_sub_Iio'
+ integral_Ioi_sub_Ioi
+ integral_Ioi_sub_Ioi'
+ inter
+ inter.isCompactSystem
+ inter.mem_iff
+ irreducible_min_polynomial_valuation_lt_one_and_ne_zero
+ one_le_valuation_factor
+ setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty
+ uniformizingPolynomial
+ uniformizingPolynomial_isUniformizer
+ uniformizingPolynomial_ne_zero
+ valuationIdeal
+ valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X
+ valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one
+ valuation_isEquiv_adic_of_not_isEquiv_infty
+ valuation_isEquiv_adic_of_valuation_X_le_one
+ valuation_isEquiv_inftyValuation_of_one_lt_valuation_X
+ valuation_isEquiv_infty_or_adic
+ valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one
+ valuation_uniformizingPolynomial_lt_one
++ Set.indicator_iUnion_of_disjoint

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.

---

Increase in tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type
8699	3	backward.isDefEq

Current commit 4292dc8d1d
Reference commit 034c50cbf6

You can run this locally as

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

---

note: file Mathlib/Probability/Independence/Process.lean` was renamed to `Mathlib/Probability/Independence/Process/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

[mathlib-dependent-issues]

This PR/issue depends on:

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

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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