frontier_range_modelWithCornersEuclideanHalfSpace

English

The frontier of the range of the corner-model map 𝓡∂ n is { y | 0 = y_0 }.

Русский

Граница образа отображения модели с углами — это { y | y_0 = 0 }.

LaTeX

$$$\\operatorname{frontier}(\\mathrm{range}(\\mathcal{R}\\partial_n)) = \\{ y : y_0 = 0 \\}$$$

Lean4

theorem frontier_range_modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] :
    frontier (range (𝓡∂ n)) = {y | 0 = y 0} := by
  calc
    frontier (range (𝓡∂ n))
    _ = frontier ({y | 0 ≤ y 0}) := by
      congr!
      apply range_euclideanHalfSpace
    _ = {y | 0 = y 0} := frontier_halfSpace 2 _ _

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