English
If s ⊆ support f, then extChartAt I c '' s equals closedBall(extChartAt I c c) f.rOut ∩ range I ∩ (extChartAt I c).symm^{-1}(s).
Русский
Если s ⊆ опорного множества f, то extChartAt I c '' s равняется замкнутому шару с радиусом f.rOut в координатах extChartAt I c, пересечённому с range I и обратному изображению через симметрическую карту.
LaTeX
$$$\operatorname{extChartAt} I c '' s = \overline{\mathrm{Ball}}(\operatorname{extChartAt} I c c, f.rOut) \cap \mathrm{range}\ I \cap (\operatorname{extChartAt} I c)^{-1}(s).$$$
Lean4
theorem image_eq_inter_preimage_of_subset_support {s : Set M} (hs : s ⊆ support f) :
extChartAt I c '' s = closedBall (extChartAt I c c) f.rOut ∩ range I ∩ (extChartAt I c).symm ⁻¹' s :=
by
rw [support_eq_inter_preimage, subset_inter_iff, ← extChartAt_source I, ← image_subset_iff] at hs
obtain ⟨hse, hsf⟩ := hs
apply Subset.antisymm
· refine subset_inter (subset_inter (hsf.trans ball_subset_closedBall) ?_) ?_
· rintro _ ⟨x, -, rfl⟩; exact mem_range_self _
· rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]
exact inter_subset_right
· refine Subset.trans (inter_subset_inter_left _ f.closedBall_subset) ?_
rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]
