English
The set image (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) is compact.
Русский
Образ (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) компакт Hen.
LaTeX
$$IsCompact (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I).$$
Lean4
/-- If `f` is a smooth bump function and `s` closed subset of the support of `f` (i.e., of the open
ball of radius `f.rOut`), then there exists `0 < r < f.rOut` such that `s` is a subset of the open
ball of radius `r`. Formally, `s ⊆ e.source ∩ e ⁻¹' (ball (e c) r)`, where `e = extChartAt I c`. -/
theorem exists_r_pos_lt_subset_ball {s : Set M} (hsc : IsClosed s) (hs : s ⊆ support f) :
∃ r ∈ Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ extChartAt I c ⁻¹' ball (extChartAt I c c) r :=
by
set e := extChartAt I c
have : IsClosed (e '' s) := f.isClosed_image_of_isClosed hsc hs
rw [support_eq_inter_preimage, subset_inter_iff, ← image_subset_iff] at hs
rcases exists_pos_lt_subset_ball f.rOut_pos this hs.2 with ⟨r, hrR, hr⟩
exact ⟨r, hrR, subset_inter hs.1 (image_subset_iff.1 hr)⟩
