Icc_isBoundaryPoint_bot — Mathlib

English

The bottom endpoint ⊥ of the interval Icc x y is a boundary point for the model with corners along the left chart.

Русский

Нижняя граница ⊥ для множества Icc x y является краевой точкой в рамках модели с углами для левого графика.

LaTeX

$$(\mathcal{R}\partial 1).IsBoundaryPoint (⊥ : Set.Icc x y)$$

Lean4

theorem Icc_isBoundaryPoint_bot : (𝓡∂ 1).IsBoundaryPoint (⊥ : Set.Icc x y) :=
  by
  rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt, Icc_chartedSpaceChartAt_of_le_top (by simp [hxy.out])]
  exact IccLeftChart_extend_bot_mem_frontier

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