ball_subset — Mathlib

English

A geometric containment: a ball around the image of the chart lies inside the chart target region.

Русский

Геометрическое включение: окружность вокруг образа графа лежит внутри области мишени графа.

LaTeX

$$$ball(extChartAt I c\\,c)\\cap range I ⊆ (extChartAt I c).target$$$

Lean4

theorem ball_subset : ball (extChartAt I c c) f.rOut ∩ range I ⊆ (extChartAt I c).target :=
  Subset.trans (inter_subset_inter_left _ ball_subset_closedBall) f.closedBall_subset

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