English
The interior of the disjoint union M ⊕ M' is the union of the images of the interiors of M and M'.
Русский
Внутренняя часть несмкщенного объединения M ⊕ M' равна объединению образов внутренних точек M и M'.
LaTeX
$$ModelWithCorners.interior (Sum M M') = Sum.inl '' (ModelWithCorners.interior M) ∪ Sum.inr '' (ModelWithCorners.interior M')$$
Lean4
theorem interior_disjointUnion :
ModelWithCorners.interior (I := I) (M ⊕ M') =
Sum.inl '' (ModelWithCorners.interior (I := I) M) ∪ Sum.inr '' (ModelWithCorners.interior (I := I) M') :=
by
ext p
constructor
· intro hp
by_cases h : Sum.isLeft p
· left
exact ⟨Sum.getLeft p h, isInteriorPoint_disjointUnion_left hp h, Sum.inl_getLeft p h⟩
· replace h := Sum.not_isLeft.mp h
right
exact ⟨Sum.getRight p h, isInteriorPoint_disjointUnion_right hp h, Sum.inr_getRight p h⟩
· intro hp
by_cases h : Sum.isLeft p
· set x := Sum.getLeft p h with x_eq
rw [Sum.eq_left_getLeft_of_isLeft h]
apply interiorPoint_inl x
have hp : p ∈ Sum.inl '' (ModelWithCorners.interior (I := I) M) :=
by
obtain (good | ⟨y, hy, hxy⟩) := hp
exacts [good, (not_isLeft_and_isRight ⟨h, by rw [← hxy]; exact rfl⟩).elim]
obtain ⟨x', hx', hx'p⟩ := hp
simpa [x_eq, ← hx'p, Sum.getLeft_inl]
· set x := Sum.getRight p (Sum.not_isLeft.mp h) with x_eq
rw [Sum.eq_right_getRight_of_isRight (Sum.not_isLeft.mp h)]
apply interiorPoint_inr x
have hp : p ∈ Sum.inr '' (ModelWithCorners.interior (I := I) M') :=
by
obtain (⟨y, hy, hxy⟩ | good) := hp
exacts [(not_isLeft_and_isRight ⟨by rw [← hxy]; exact rfl, Sum.not_isLeft.mp h⟩).elim, good]
obtain ⟨x', hx', hx'p⟩ := hp
simpa [x_eq, ← hx'p, Sum.getRight_inr]
