Compact-system compatibility for the pinned Mathlib

The eight declarations below are copied from Mathlib commit e91b128082cc221d6432a6a5aadcd3243af8e76c, retaining their statements and proofs. They supply the compact-system API needed by KolmogorovExtension4 over Mathlib 56a005855ea17e0b0958f73ec801ae140b0a1679.

Sources:

• Mathlib/Data/Set/Lattice/Bounded.lean, lines 600–603 and 616–622;
• Mathlib/Topology/Compactness/CompactSystem.lean, lines 199–252 and 269–300.

theorem Set.iInter_pi {α : Type u_1} {ι : Sort u_2} {π : α → Type u_3} (t : ι → (a : α) → Set (π a)) (s : Set α) : ⋂ (i : ι), s.pi (t i) = s.pi fun (a : α) => ⋂ (i : ι), t i a

theorem Set.iInter_univ_pi_eq_empty_iff {α : Type u_1} {ι : Sort u_2} {π : α → Type u_3} {t : ι → (a : α) → Set (π a)} : ⋂ (i : ι), univ.pi (t i) = ∅ ↔ ∃ (a : α), ⋂ (i : ι), t i a = ∅

theorem Set.biInter_univ_pi_eq_empty_iff {α : Type u_1} {ι : Sort u_2} {π : α → Type u_3} {t : ι → (a : α) → Set (π a)} {p : ι → Prop} : ⋂ (i : ι), ⋂ (_ : p i), univ.pi (t i) = ∅ ↔ ∃ (a : α), ⋂ (i : ι), ⋂ (_ : p i), t i a = ∅

theorem IsCompactSystem.supClosure {α : Type u_1} {S : Set (Set α)} (hS : IsCompactSystem S) : IsCompactSystem (supClosure S)

If S is a compact system, then so is the set of finite unions of sets in S.

theorem IsCompactSystem.countableInfClosure {α : Type u_1} {S : Set (Set α)} (hS : IsCompactSystem S) : IsCompactSystem (countableInfClosure S)

If S is a compact system, then the set of countable intersections of sets in S is also a compact system.

theorem IsCompactSystem.pi {ι : Type u_2} {α : ι → Type u_3} {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), IsCompactSystem (C i)) : IsCompactSystem (Set.univ.pi '' Set.univ.pi C)

Boxes formed by compact systems form a compact system.

def compactClosedSquareCylinders {ι : Type u_2} (α : ι → Type u_3) [(i : ι) → TopologicalSpace (α i)] : Set (Set ((i : ι) → α i))

The set of sets of the form s.pi t, where s : Finset ι and t i is both closed and compact for all i ∈ s.

Equations

• compactClosedSquareCylinders α = MeasureTheory.squareCylinders fun (i : ι) => {t : Set (α i) | IsCompact t ∧ IsClosed t}

theorem isCompactSystem_compactClosedSquareCylinders {ι : Type u_2} (α : ι → Type u_3) [(i : ι) → TopologicalSpace (α i)] : IsCompactSystem (compactClosedSquareCylinders α)

Compact and closed square cylinders form a compact system.