English
The image of a compact set under projection to the i-th coordinate is closed.
Русский
Образ компактного множества по i-ой координате замкнут.
LaTeX
$$$\\text{IsClosed}(\\{x \\in s : x_i \\in ?\\})$ given compactness of s; i-th coordinate image is closed.$$
Lean4
theorem isClosed_image_eval (i : ι) (hs_compact : IsCompact s) (hs_closed : IsClosed s) :
IsClosed ((fun x ↦ x i) '' s) :=
by
suffices IsClosed (Set.restrict { i } '' s)
by
have : Homeomorph.piUnique _ ∘ Set.restrict { i } = fun (x : Π j, α j) ↦ x i := rfl
rwa [← this, image_comp, Homeomorph.isClosed_image (Homeomorph.piUnique _)]
exact hs_compact.isClosed_image_restrict { i } hs_closed