English
The product of two compact spaces is compact: if s ⊆ X and t ⊆ Y are compact, then s × t is compact in X × Y.
Русский
Произведение двух компактных пространств компактно: если s ⊆ X и t ⊆ Y компактны, то s × t компактно в X × Y.
LaTeX
$$$\IsCompact\,s \to \IsCompact\,t \Rightarrow \IsCompact\,(s \times\! t)$$$
Lean4
theorem prod {t : Set Y} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ×ˢ t) :=
by
rw [isCompact_iff_ultrafilter_le_nhds'] at hs ht ⊢
intro f hfs
obtain ⟨x : X, sx : x ∈ s, hx : map Prod.fst f.1 ≤ 𝓝 x⟩ :=
hs (f.map Prod.fst) (mem_map.2 <| mem_of_superset hfs fun x => And.left)
obtain ⟨y : Y, ty : y ∈ t, hy : map Prod.snd f.1 ≤ 𝓝 y⟩ :=
ht (f.map Prod.snd) (mem_map.2 <| mem_of_superset hfs fun x => And.right)
rw [map_le_iff_le_comap] at hx hy
refine ⟨⟨x, y⟩, ⟨sx, ty⟩, ?_⟩
rw [nhds_prod_eq]; exact le_inf hx hy
