union' — Mathlib

English

If s ∩ t is nonempty and both s and t are preconnected, then s ∪ t is preconnected.

Русский

Если пересечение s и t непусто и оба множества предсоединены, то их объединение предсоединено.

LaTeX

$$$$ \\operatorname{IsPreconnected}(s) \\wedge \\operatorname{IsPreconnected}(t) \\wedge (s \\cap t) \\neq \\emptyset \\Rightarrow \\operatorname{IsPreconnected}(s \\cup t). $$$$

Lean4

theorem union' {s t : Set α} (H : (s ∩ t).Nonempty) (hs : IsPreconnected s) (ht : IsPreconnected t) :
    IsPreconnected (s ∪ t) := by
  rcases H with ⟨x, hxs, hxt⟩
  exact hs.union x hxs hxt ht

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