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