Theorems · Definition · general topology

DiscreteQuotient.equivFinsetClopens

(X : Type u_2) →
  [inst : TopologicalSpace X] →
    [inst_1 : CompactSpace X] → DiscreteQuotient X ≃ ↑(Set.range (DiscreteQuotient.finsetClopens X))

The discrete quotients of a compact space are in bijection with a subtype of the type of Finset (Clopens X). TODO: show that this is precisely those finsets of clopens which form a partition of X.

Defined in

Mathlib.Topology.DiscreteQuotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCompactSpace