English
Every clopen subset W of X × Y (compact spaces) can be expressed as a finite supremum of products of clopen subsets of X and Y.
Русский
Каждое клиopen-подмножество W пространства X×Y (компактные пространства) представимо как конечная супрема (объединение) произведений клиopen-множест X и Y.
LaTeX
$$$$ \exists I : \mathrm{Finset}(\mathrm{Clopens}(X) \times \mathrm{Clopens}(Y)), \, W = I \mathbin{\uparrow}\, (\lambda i. i.1 \timesˢ i.2) $$$$
Lean4
/-- Every clopen set in a product of two compact spaces
is a union of finitely many clopen boxes. -/
theorem exists_finset_eq_sup_prod (W : Clopens (X × Y)) :
∃ (I : Finset (Clopens X × Clopens Y)), W = I.sup fun i ↦ i.1 ×ˢ i.2 :=
by
choose! U hxU V hxV hUV using fun x ↦ W.exists_prod_subset (a := x)
rcases
W.2.1.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x)
(fun x hx ↦ (U x ×ˢ V x).2.isOpen.mem_nhds ⟨hxU x hx, hxV x hx⟩) with
⟨I, hIW, hWI⟩
classical
use I.image fun x ↦ (U x, V x)
rw [Finset.sup_image]
refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
· rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
exact SetLike.le_def.1 (Finset.le_sup hi) hxi
· exact hUV _ <| hIW _ hx
