Locally compact Stone duality

Tristan Bice and Charles Starling

It is proved that "Compact clopen pseudobasic posets are characterized by separativity."

As a first formal step in that direction we prove some basic results about clopen sets.

theorem clopenness_true {i : ℕ} : IsClopen {A : ℕ → Bool | A i = true}

theorem clopenness_false {i : ℕ} : IsClopen {A : ℕ → Bool | A i = false}

theorem clopenness {i : ℕ} {b : Bool} : IsClopen {A : ℕ → Bool | A i = b}