isClosed_image_eval — Mathlib

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

Похожие утверждения