isCompact_symm_image_closedBall — Mathlib

English

The family of sets closedBall((extChartAt I c).toFun c, r) ∩ range I, as r varies, forms a basis of the nhds at range I.

Русский

Семейство замкнутых шаров в координатах extChartAt, пересечённых с range I, образует базис окрестностей в точке range I.

LaTeX

$$$(\mathcal{nhdsWithin} (\mathrm{extChartAt} I c).toFun c).HasBasis (fun f => True) (fun f => \overline{B}(\mathrm{extChartAt} I c c, f.rOut) \cap \mathrm{range} I).$$$

Lean4

theorem isCompact_symm_image_closedBall :
    IsCompact ((extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I)) :=
  ((isCompact_closedBall _ _).inter_right I.isClosed_range).image_of_continuousOn <|
    (continuousOn_extChartAt_symm _).mono f.closedBall_subset

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