Theorems · Theorem · general topology

exists_clopen_partition_of_clopen_cover

∀ {X : Type u_4} {I : Type u_5} [inst : TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
  [Finite I] {Z D : I → Set X},
  (∀ (i : I), IsClosed (Z i)) →
    (∀ (i : I), IsClopen (D i)) →
      (∀ (i : I), Z i ⊆ D i) →
        Set.univ.PairwiseDisjoint Z →
          ∃ C,
            (∀ (i : I), IsClopen (C i)) ∧
              (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ Set.univ.PairwiseDisjoint C

Let X be a totally disconnected compact Hausdorff space, D i ⊆ X a finite family of clopens, and Z i ⊆ D i closed. Assume that the Z i are pairwise disjoint. Then there exist clopens Z i ⊆ C i ⊆ D i with the C i disjoint, and such that ∪ D i ⊆ ∪ C i.

Defined in

Mathlib.Topology.Separation.Profinite

Cited by

1 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceCompactSpaceT2SpaceTotallyDisconnectedSpaceFinite