interior_range_modelWithCornersEuclideanHalfSpace

English

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

Русский

interior образа отображения модели с углами равен { y | 0 < y_0 }.

LaTeX

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

Lean4

theorem interior_range_modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] :
    interior (range (𝓡∂ n)) = {y | 0 < y 0} := by
  calc
    interior (range (𝓡∂ n))
    _ = interior ({y | 0 ≤ y 0}) := by
      congr!
      apply range_euclideanHalfSpace
    _ = {y | 0 < y 0} := interior_halfSpace _ _ _

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