isClosed_image_of_isClosed — Mathlib

English

If s is closed and s ⊆ support f, then the image extChartAt I c '' s is closed.

Русский

Если s замкнуто и s ⊆ опорного множества f, то образ extChartAt I c '' s замкнуто.

LaTeX

$$IsClosed (extChartAt I c '' s) given IsClosed s and s ⊆ support f.$$

Lean4

theorem isClosed_image_of_isClosed {s : Set M} (hsc : IsClosed s) (hs : s ⊆ support f) :
    IsClosed (extChartAt I c '' s) :=
  by
  rw [f.image_eq_inter_preimage_of_subset_support hs]
  refine ContinuousOn.preimage_isClosed_of_isClosed ((continuousOn_extChartAt_symm _).mono f.closedBall_subset) ?_ hsc
  exact IsClosed.inter isClosed_closedBall I.isClosed_range

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