IccRightChart_extend_top_mem_frontier

English

The top element of the right chart extension lies in the frontier of the image range of the extension map.

Русский

Вершина верхнего элемента продления правого графика принадлежит границе образа функции расширения.

LaTeX

$$(IccRightChart x y).extend (\mathcal{R}\partial 1) \top ∈ \operatorname{frontier}(\operatorname{range}(\mathcal{R}\partial 1))$$

Lean4

theorem IccRightChart_extend_top_mem_frontier : (IccRightChart x y).extend (𝓡∂ 1) ⊤ ∈ frontier (range (𝓡∂ 1)) := by
  rw [IccRightChart_extend_top, frontier_range_modelWithCornersEuclideanHalfSpace, mem_setOf, PiLp.zero_apply]

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