instBoundarylessManifold — Mathlib

English

I.IsInteriorPoint x is equivalent to extChartAt I x x ∈ interior (extChartAt I x).target.

Русский

I.IsInteriorPoint x эквивалентно extChartAt I x x ∈ interior (extChartAt I x).target.

LaTeX

$$$$ I.IsInteriorPoint x \iff extChartAt I x x \in interior ((extChartAt I x).target) $$$$

Lean4

/-- Boundaryless `ModelWithCorners` implies boundaryless manifold. -/
instance : BoundarylessManifold I M where
  isInteriorPoint'
    x := by
    let r := ((chartAt H x).isOpen_extend_target (I := I)).interior_eq
    have : extChartAt I x = (chartAt H x).extend I := rfl
    rw [← this] at r
    rw [isInteriorPoint_iff, r]
    exact PartialEquiv.map_source _ (mem_extChartAt_source _)

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