IccLeftChart_extend_bot — Mathlib

English

The extension of IccLeftChart to the corner along the bottom edge equals 0.

Русский

Расширение IccLeftChart до угла по нижней грани равно 0.

LaTeX

$$$((\\mathrm{IccLeftChart}(x,y)).\\mathrm{extend}(\\mathrm{modelWithCornersEuclideanHalfSpace}(1))).\\mathrm{toFun} (\\mathrm{Bot}.bot) = 0$$$

Lean4

theorem IccLeftChart_extend_bot : (IccLeftChart x y).extend (𝓡∂ 1) ⊥ = 0 :=
  by
  norm_num [IccLeftChart, modelWithCornersEuclideanHalfSpace_zero]
  congr

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