English
In a product X × Y of compact spaces, every clopen subset W corresponds to a finite collection of clopen boxes U ×ˢ V with W containing U ×ˢ V and the W-status is captured by a finite subcover.
Русский
В произведении X×Y двух компактных пространств каждый клиopen-набор W можно разбить на конечную коллекцию клиopen-ящиков U×V, таких что W содержит U×V и описывает покрытие.
LaTeX
$$$$ \exists U \in \text{Clopens}(X), \exists V \in \text{Clopens}(Y), U \times V \subseteq W \;\wedge\; \dots $$$$
Lean4
theorem exists_prod_subset (W : Clopens (X × Y)) {a : X × Y} (h : a ∈ W) :
∃ U : Clopens X, a.1 ∈ U ∧ ∃ V : Clopens Y, a.2 ∈ V ∧ U ×ˢ V ≤ W :=
by
have hp : Continuous (fun y : Y ↦ (a.1, y)) := .prodMk_right _
let V : Set Y := {y | (a.1, y) ∈ W}
have hV : IsCompact V := (W.2.1.preimage hp).isCompact
let U : Set X := {x | MapsTo (Prod.mk x) V W}
have hUV : U ×ˢ V ⊆ W := fun ⟨_, _⟩ hw ↦ hw.1 hw.2
exact
⟨⟨U, (ContinuousMap.isClopen_setOf_mapsTo hV W.2).preimage (ContinuousMap.id (X × Y)).curry.2⟩, by
simp [U, V, MapsTo], ⟨V, W.2.preimage hp⟩, h, hUV⟩
