IccLeftChart_extend_bot_mem_frontier

English

The bottom endpoint element ⊥ of the left-extended chart lies on the frontier of the image range of the extension map.

Русский

Нижняя граница элемента ⊥ левого расширения лежит на границе образа отображения расширения.

LaTeX

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

Lean4

theorem IccLeftChart_extend_bot_mem_frontier : (IccLeftChart x y).extend (𝓡∂ 1) ⊥ ∈ frontier (range (𝓡∂ 1)) := by
  rw [IccLeftChart_extend_bot, frontier_range_modelWithCornersEuclideanHalfSpace, mem_setOf, PiLp.zero_apply]

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