Clopen subsets in cartesian products

In general, a clopen subset in a cartesian product of topological spaces cannot be written as a union of "clopen boxes", i.e. products of clopen subsets of the components (see [Buz01] for counterexamples).

However, when one of the factors is compact, a clopen subset can be written as such a union. Our argument in TopologicalSpace.Clopens.exists_prod_subset follows the one given in [Buz01].

We deduce that in a product of compact spaces, a clopen subset is a finite union of clopen boxes, and use that to prove that the property of having countably many clopens is preserved by taking cartesian products of compact spaces (this is relevant to the theory of light profinite sets).

References

• [Buz01]: On clopen sets in Cartesian products, 2001.
• [Eng89]: General Topology, 1989.

theorem TopologicalSpace.Clopens.exists_prod_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] (W : TopologicalSpace.Clopens (X × Y)) {a : X × Y} (h : a ∈ W) : ∃ (U : TopologicalSpace.Clopens X), a.1 ∈ U ∧ ∃ (V : TopologicalSpace.Clopens Y), a.2 ∈ V ∧ U ×ˢ V ≤ W

theorem TopologicalSpace.Clopens.exists_finset_eq_sup_prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] [CompactSpace X] (W : TopologicalSpace.Clopens (X × Y)) : ∃ (I : Finset (TopologicalSpace.Clopens X × TopologicalSpace.Clopens Y)), W = I.sup fun (i : TopologicalSpace.Clopens X × TopologicalSpace.Clopens Y) => i.1 ×ˢ i.2

Every clopen set in a product of two compact spaces is a union of finitely many clopen boxes.

theorem TopologicalSpace.Clopens.surjective_finset_sup_prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] [CompactSpace X] : Function.Surjective fun (I : Finset (TopologicalSpace.Clopens X × TopologicalSpace.Clopens Y)) => I.sup fun (i : TopologicalSpace.Clopens X × TopologicalSpace.Clopens Y) => i.1 ×ˢ i.2

instance TopologicalSpace.Clopens.countable_prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] [CompactSpace X] [Countable (TopologicalSpace.Clopens X)] [Countable (TopologicalSpace.Clopens Y)] : Countable (TopologicalSpace.Clopens (X × Y))

instance TopologicalSpace.Clopens.finite_prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] [CompactSpace X] [Finite (TopologicalSpace.Clopens X)] [Finite (TopologicalSpace.Clopens Y)] : Finite (TopologicalSpace.Clopens (X × Y))

theorem TopologicalSpace.Clopens.countable_iff_secondCountable {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] : Countable (TopologicalSpace.Clopens X) ↔ SecondCountableTopology X

@[deprecated TopologicalSpace.Clopens.countable_iff_secondCountable]

theorem TopologicalSpace.Clopens.countable_iff_second_countable {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] : Countable (TopologicalSpace.Clopens X) ↔ SecondCountableTopology X

Alias of TopologicalSpace.Clopens.countable_iff_secondCountable.