isInteriorPoint_disjointUnion_right

English

The interior of the disjoint union M ⊕ M' equals the union of the images of the interiors of M and M'.

Русский

Внутренность нессмещённого объединения M ⊕ M' равна объединению образов внутренних точек M и M'.

LaTeX

$$ModelWithCorners.interior (I := I) (M ⊕ M') = Sum.inl '' (ModelWithCorners.interior (I := I) M) ∪ Sum.inr '' (ModelWithCorners.interior (I := I) M')$$

Lean4

theorem isInteriorPoint_disjointUnion_right {p : M ⊕ M'} (hp : I.IsInteriorPoint p) (hright : Sum.isRight p) :
    I.IsInteriorPoint (Sum.getRight p hright) := by
  by_contra h
  set x := Sum.getRight p hright
  rw [← mem_empty_iff_false p, ← (disjoint_interior_boundary (I := I)).inter_eq]
  constructor
  · rw [ModelWithCorners.interior, mem_setOf]; exact hp
  · rw [ModelWithCorners.boundary, mem_setOf, Sum.eq_right_getRight_of_isRight hright]
    have := isInteriorPoint_or_isBoundaryPoint (I := I) x
    exact boundaryPoint_inr (M' := M') x (by tauto)

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