interiorPoint_inr — Mathlib

English

If x is interior in M', then Sum.inr x is interior in M ⊕ M'.

Русский

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

LaTeX

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

Lean4

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

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