Icc_isBoundaryPoint_top — Mathlib

English

The boundary of the Icc interval [x,y] consists precisely of the two endpoints, i.e., ⊥ and ⊤ in the endpoint ordering.

Русский

Граница отрезка [x,y] состоит ровно из двух концов: ⊥ и ⊤ в соответствующем упорядочении концов.

LaTeX

$$\partial([x,y]) = {⊥, ⊤}$$

Lean4

theorem Icc_isBoundaryPoint_top : (𝓡∂ 1).IsBoundaryPoint (⊤ : Set.Icc x y) :=
  by
  rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt, Icc_chartedSpaceChartAt_of_top_le (by simp)]
  exact IccRightChart_extend_top_mem_frontier

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