support_eq_symm_image — Mathlib

English

The support of f equals the symmetric-image form: extChartAt I c .symm '' (ball (extChartAt I c c) f.rOut ∩ range I).

Русский

Опорное множество f совпадает с симметрическим образом extChartAt I c .symm '' (ball (extChartAt I c c) f.rOut ∩ range I).

LaTeX

$$$\operatorname{support}(f) = (\operatorname{extChartAt} I c).\mathrm{symm} '' (\mathrm{ball}(\operatorname{extChartAt} I c c, f.rOut) \cap \mathrm{range}\ I).$$$

Lean4

theorem support_eq_symm_image : support f = (extChartAt I c).symm '' (ball (extChartAt I c c) f.rOut ∩ range I) := by
  rw [f.support_eq_inter_preimage, ← extChartAt_source I, ← (extChartAt I c).symm_image_target_inter_eq', inter_comm,
    ball_inter_range_eq_ball_inter_target]

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