boundaryPoint_inr — Mathlib

English

If x is a boundary point in M', Sum.inr x is a boundary point in M ⊕ M'.

Русский

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

LaTeX

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

Lean4

theorem boundaryPoint_inr (x : M') (hx : I.IsBoundaryPoint x) : I.IsBoundaryPoint (.inr x : M ⊕ M') :=
  by
  rw [I.isBoundaryPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inr]
  dsimp
  rw [Sum.inr_injective.extend_apply (chartAt H x)]
  simpa [I.isBoundaryPoint_iff, extChartAt] using hx

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