isInteriorPoint_iff — Mathlib

English

For a point x, I.IsInteriorPoint x is equivalent to extChartAt I x x being in the interior of the model space target.

Русский

Для точки x условие I.IsInteriorPoint x эквивалентно тому, что extChartAt I x x лежит во внутренности целевого моделируемого пространства.

LaTeX

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

Lean4

theorem isInteriorPoint_iff {x : M} : I.IsInteriorPoint x ↔ extChartAt I x x ∈ interior (extChartAt I x).target :=
  ⟨fun h ↦ (chartAt H x).mem_interior_extend_target (mem_chart_target H x) h, fun h ↦
    OpenPartialHomeomorph.interior_extend_target_subset_interior_range _ h⟩

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