union — Mathlib

English

If x ∈ s ∩ t and s,t are preconnected, then s ∪ t is preconnected.

Русский

Если x ∈ s ∩ t и s,t предсоединены, то s ∪ t предсоединено.

LaTeX

$$$$ x\\in s\\cap t\\;\\&\\; \\operatorname{IsPreconnected}(s) \\;\\&\\; \\operatorname{IsPreconnected}(t) \\Rightarrow \\operatorname{IsPreconnected}(s\\cup t). $$$$

Lean4

theorem union (x : α) {s t : Set α} (H1 : x ∈ s) (H2 : x ∈ t) (H3 : IsPreconnected s) (H4 : IsPreconnected t) :
    IsPreconnected (s ∪ t) :=
  sUnion_pair s t ▸
    isPreconnected_sUnion x { s, t } (by rintro r (rfl | rfl | h) <;> assumption)
      (by rintro r (rfl | rfl | h) <;> assumption)

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