union — Mathlib

English

If U and V are path-connected subsets with nonempty intersection, then U ∪ V is path-connected.

Русский

Если U и V — пути-связные подмножества, обладающие непустым пересечением, то U ∪ V является путево связным.

LaTeX

$$IsPathConnected(U \cup V)$$

Lean4

theorem union {U V : Set X} (hU : IsPathConnected U) (hV : IsPathConnected V) (hUV : (U ∩ V).Nonempty) :
    IsPathConnected (U ∪ V) := by
  rcases hUV with ⟨x, xU, xV⟩
  use x, Or.inl xU
  rintro y (yU | yV)
  · exact (hU.joinedIn x xU y yU).mono subset_union_left
  · exact (hV.joinedIn x xV y yV).mono subset_union_right

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