Icc_isInteriorPoint_interior — Mathlib

English

If p lies strictly between x and y, then p is an interior point with respect to the left chart structure from the model with corners.

Русский

Если p лежит строго между x и y, то p является внутренней точкой относительно структуры левого графика в модели с углами.

LaTeX

$$(Icc x y).IsInteriorPoint(p) \;\text{ if } x < p < y$$

Lean4

theorem Icc_isInteriorPoint_interior {p : Set.Icc x y} (hp : x < p.val ∧ p.val < y) : (𝓡∂ 1).IsInteriorPoint p :=
  by
  rw [ModelWithCorners.IsInteriorPoint, extChartAt, Icc_chartedSpaceChartAt_of_le_top hp.2,
    interior_range_modelWithCornersEuclideanHalfSpace]
  exact IccLeftChart_extend_interior_pos hp

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