isInteriorPoint_disjointUnion_left

English

If p ∈ M ⊕ M' is interior, then the left projection is interior (with the left witness).

Русский

Если p внутри в M ⊕ M' и принадлежит левой части, то её проекция внутри.

LaTeX

$$I.IsInteriorPoint p \Rightarrow ∀ hleft, I.IsInteriorPoint (p.getLeft hleft)$$

Lean4

theorem isInteriorPoint_disjointUnion_left {p : M ⊕ M'} (hp : I.IsInteriorPoint p) (hleft : Sum.isLeft p) :
    I.IsInteriorPoint (Sum.getLeft p hleft) := by
  by_contra h
  set x := Sum.getLeft p hleft
  rw [isInteriorPoint_iff_not_isBoundaryPoint x, not_not] at h
  rw [isInteriorPoint_iff_not_isBoundaryPoint p] at hp
  have := boundaryPoint_inl (M' := M') x (by tauto)
  rw [← Sum.eq_left_getLeft_of_isLeft hleft] at this
  exact hp this

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