interiorPoint_inl — Mathlib

English

If x is an interior point of M, then the left-injected point Sum.inl x is interior in M ⊕ M'.

Русский

Если x является внутренней точкой M, то Sum.inl x является внутренней точкой в M ⊕ M'.

LaTeX

$$I.IsInteriorPoint x \Rightarrow I.IsInteriorPoint (Sum.inl x)$$

Lean4

theorem interiorPoint_inl (x : M) (hx : I.IsInteriorPoint x) : I.IsInteriorPoint (.inl x : M ⊕ M') :=
  by
  rw [I.isInteriorPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inl]
  dsimp
  rw [Sum.inl_injective.extend_apply (chartAt H x)]
  simpa [I.isInteriorPoint_iff, extChartAt] using hx

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