isInteriorPoint_or_isBoundaryPoint

English

Every point of the manifold is either an interior point or a boundary point.

Русский

Каждая точка многообразия либо внутри, либо на границе.

LaTeX

$$$$ \forall x \in M, I.IsInteriorPoint x \lor I.IsBoundaryPoint x $$$$

Lean4

/-- Every point is either an interior or a boundary point. -/
theorem isInteriorPoint_or_isBoundaryPoint (x : M) : I.IsInteriorPoint x ∨ I.IsBoundaryPoint x :=
  by
  rw [IsInteriorPoint, or_iff_not_imp_left, I.isBoundaryPoint_iff, ← closure_diff_interior, I.isClosed_range.closure_eq,
    mem_diff]
  exact fun h ↦ ⟨mem_range_self _, h⟩

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