boundaryPoint_inl — Mathlib

English

If x is a boundary point of M, then Sum.inl x is a boundary point of M ⊕ M'.

Русский

Если x — точка границы M, то Sum.inl x — точка границы в M ⊕ M'.

LaTeX

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

Lean4

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

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