ball_inter_range_eq_ball_inter_target

English

Intersections with the image range and target coincide for the ball around the chart center.

Русский

Пересечение с областью Range совпадает с пересечением с Target.

LaTeX

$$$ball(extChartAt I c).toFun c)\\cap range I = ball(extChartAt I c).toFun c)\\cap (extChartAt I c).target$$$

Lean4

theorem ball_inter_range_eq_ball_inter_target :
    ball (extChartAt I c c) f.rOut ∩ range I = ball (extChartAt I c c) f.rOut ∩ (extChartAt I c).target :=
  (subset_inter inter_subset_left f.ball_subset).antisymm <|
    inter_subset_inter_right _ <| extChartAt_target_subset_range _

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