Compact systems

This file defines compact systems of sets.

Main definitions

• IsCompactSystem: A set of sets is a compact system if, whenever a countable subfamily has empty intersection, then finitely many of them already have empty intersection.
• compactClosedSquareCylinders: The square cylinders in a product space whose sides are compact and closed.

Main results

• isCompactSystem_insert_univ_iff: A set system is a compact system iff inserting univ gives a compact system.
• isCompactSystem_isCompact_isClosed: The set of closed and compact sets is a compact system.
• isCompactSystem_isCompact: In a T2Space, the set of compact sets is a compact system.
• IsCompactSystem.supClosure: If S is a compact system, then the set of finite unions of sets in S is also a compact system.
• IsCompactSystem.countableInfClosure: If S is a compact system, then the set of countable intersections of sets in S is a compact system.
• IsCompactSystem.prod, IsCompactSystem.pi: Products of sets from compact systems form a compact system.
• isCompactSystem_compactClosedSquareCylinders: Compact and closed square cylinders form a compact system.

def IsCompactSystem {α : Type u_1} (S : Set (Set α)) : Prop

A set of sets is a compact system if, whenever a countable subfamily has empty intersection, then finitely many of them already have empty intersection.

Equations

• IsCompactSystem S = ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → ⋂ (i : ℕ), C i = ∅ → ∃ (n : ℕ), Set.dissipate C n = ∅

theorem IsCompactSystem.of_nonempty_iInter {α : Type u_1} {S : Set (Set α)} (h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (Set.dissipate C n).Nonempty) → (⋂ (i : ℕ), C i).Nonempty) : IsCompactSystem S

theorem IsCompactSystem.nonempty_iInter {α : Type u_1} {S : Set (Set α)} (hp : IsCompactSystem S) {C : ℕ → Set α} (hC : ∀ (i : ℕ), C i ∈ S) (h_nonempty : ∀ (n : ℕ), (Set.dissipate C n).Nonempty) : (⋂ (i : ℕ), C i).Nonempty

theorem IsCompactSystem.iff_nonempty_iInter {α : Type u_1} (S : Set (Set α)) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (Set.dissipate C n).Nonempty) → (⋂ (i : ℕ), C i).Nonempty

@[simp]

theorem IsCompactSystem.of_IsEmpty {α : Type u_1} [IsEmpty α] (S : Set (Set α)) : IsCompactSystem S

theorem IsCompactSystem.mono {α : Type u_1} {S T : Set (Set α)} (hT : IsCompactSystem T) (hST : S ⊆ T) : IsCompactSystem S

Any subset of a compact system is a compact system.

theorem IsCompactSystem.insert_empty {α : Type u_1} {S : Set (Set α)} (h : IsCompactSystem S) : IsCompactSystem (insert ∅ S)

Inserting ∅ into a compact system gives a compact system.

theorem IsCompactSystem.insert_univ {α : Type u_1} {S : Set (Set α)} (h : IsCompactSystem S) : IsCompactSystem (insert Set.univ S)

Inserting univ into a compact system gives a compact system.

theorem isCompactSystem_iff_nonempty_iInter_of_lt {α : Type u_1} (S : Set (Set α)) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ (k : ℕ), ⋂ (_ : k < n), C k).Nonempty) → (⋂ (i : ℕ), C i).Nonempty

In this equivalent formulation for a compact system, note that we use ⋂ k < n, C k rather than ⋂ k ≤ n, C k.

theorem isCompactSystem_insert_empty_iff {α : Type u_1} {S : Set (Set α)} : IsCompactSystem (insert ∅ S) ↔ IsCompactSystem S

A set system is a compact system iff adding ∅ gives a compact system.

theorem isCompactSystem_insert_univ_iff {α : Type u_1} {S : Set (Set α)} : IsCompactSystem (insert Set.univ S) ↔ IsCompactSystem S

A set system is a compact system iff adding univ gives a compact system.

theorem isCompactSystem_iff_of_directed {α : Type u_1} {S : Set (Set α)} (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ (i : ℕ), C i = ∅ → ∃ (n : ℕ), C n = ∅

To prove that a set of sets is a compact system, it suffices to consider directed families of sets.

theorem isCompactSystem_iff_nonempty_iInter_of_directed {α : Type u_1} {S : Set (Set α)} (hpi : IsPiSystem S) : IsCompactSystem S ↔ ∀ (C : ℕ → Set α), Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → (⋂ (i : ℕ), C i).Nonempty

To prove that a set of sets is a compact system, it suffices to consider directed families of sets.

theorem isCompactSystem_isCompact_isClosed (α : Type u_2) [TopologicalSpace α] : IsCompactSystem {s : Set α | IsCompact s ∧ IsClosed s}

The set of compact and closed sets is a compact system.

theorem isCompactSystem_isCompact (α : Type u_2) [TopologicalSpace α] [T2Space α] : IsCompactSystem {s : Set α | IsCompact s}

In a T2Space the set of compact sets is a compact system.

theorem isCompactSystem_insert_univ_isCompact_isClosed (α : Type u_2) [TopologicalSpace α] : IsCompactSystem (insert Set.univ {s : Set α | IsCompact s ∧ IsClosed s})

The set of sets which are either compact and closed, or univ, is a compact system.

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.prod {α : Type u_1} {S : Set (Set α)} {β : Type u_2} {T : Set (Set β)} (hS : IsCompactSystem S) (hT : IsCompactSystem T) : IsCompactSystem (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) S T)

Products of sets from two compact systems form 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.