disjoint_interior_boundary — Mathlib

English

The interior and boundary are disjoint: I.interior M ∩ I.boundary M = ∅.

Русский

Внутренности и границы несовместны: I.interior M ∩ I.boundary M = ∅.

LaTeX

$$$$ (I.interior M) \cap (I.boundary M) = \varnothing $$$$

Lean4

/-- The interior and boundary of a manifold `M` are disjoint. -/
theorem disjoint_interior_boundary : Disjoint (I.interior M) (I.boundary M) :=
  by
  by_contra h
  obtain ⟨x, h1, h2⟩ := not_disjoint_iff.mp h
  rw [← mem_empty_iff_false (extChartAt I x x), ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier,
    mem_inter_iff]
  exact ⟨h1, h2⟩

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