union_left — Mathlib

English

If s and t are separated from u, then s ∪ t is separated from u.

Русский

Если s и t разделены от u, то s ∪ t разделены от u.

LaTeX

$$$ \mathrm{SeparatedNhds}(s,u) \land \mathrm{SeparatedNhds}(t,u) \Rightarrow \mathrm{SeparatedNhds}(s\cup t,u) $$$

Lean4

theorem union_left : SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u := by
  simpa only [separatedNhds_iff_disjoint, nhdsSet_union, disjoint_sup_left] using And.intro

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