tsupport_subset_symm_image_closedBall

English

The tsupport of f is contained in the symmetric image of a closed ball intersect range I under extChartAt.

Русский

tsupport f содержится в симметричном образе замкнутого шара, пересеченного с range I под extChartAt.

LaTeX

$$tsupport f ⊆ (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I).$$

Lean4

theorem tsupport_subset_symm_image_closedBall :
    tsupport f ⊆ (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) :=
  by
  rw [tsupport, support_eq_symm_image]
  exact
    closure_minimal (image_mono <| inter_subset_inter_left _ ball_subset_closedBall) f.isClosed_symm_image_closedBall

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