isBoundaryPoint_iff — Mathlib

English

IsInteriorPoint x is equivalent to not being a boundary point: I.IsInteriorPoint x ⇔ ¬ I.IsBoundaryPoint x.

Русский

Внутренняя точка x эквивалентна тому, что x не является граничной точкой: I.IsInteriorPoint x ⇔ ¬ I.IsBoundaryPoint x.

LaTeX

$$$$ I.IsInteriorPoint x \iff \neg I.IsBoundaryPoint x $$$$

Lean4

theorem isBoundaryPoint_iff {x : M} : I.IsBoundaryPoint x ↔ extChartAt I x x ∈ frontier (range I) :=
  Iff.rfl

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