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.

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.

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.