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⟩