union_right — Mathlib

English

If s is separated from t and s is separated from t', then s is separated from t ∪ t'.

Русский

Если S отделено от T и S отделено от T', тогда S отделено от T ∪ T'.

LaTeX

$$$ \text{AreSeparated}(s,t) \land \text{AreSeparated}(s,t') \Rightarrow \text{AreSeparated}(s, t \cup t') $$$

Lean4

theorem union_right {t'} (h : AreSeparated s t) (h' : AreSeparated s t') : AreSeparated s (t ∪ t') :=
  (h.symm.union_left h'.symm).symm

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