isInteriorPoint_iff_not_isBoundaryPoint

English

For any x, I.IsInteriorPoint x is equivalent to not I.IsBoundaryPoint x.

Русский

Для любой точки x, I.IsInteriorPoint x эквивалентно тому, что x не является граничной точкой.

LaTeX

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

Lean4

theorem isInteriorPoint_iff_not_isBoundaryPoint (x : M) : I.IsInteriorPoint x ↔ ¬I.IsBoundaryPoint x :=
  by
  refine ⟨?_, by simpa only [or_iff_not_imp_right] using isInteriorPoint_or_isBoundaryPoint x (I := I)⟩
  by_contra! h
  rw [← mem_empty_iff_false (extChartAt I x x), ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier,
    mem_inter_iff]
  exact h

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