union_right

Mathlib.Topology.Separation.SeparatedNhds

URI: https://scilib.ai/kg/mathlib#SeparatedNhds.union_right

English

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

Русский

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

LaTeX

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

Lean4

theorem union_right (ht : SeparatedNhds s t) (hu : SeparatedNhds s u) : SeparatedNhds s (t ∪ u) :=
  (ht.symm.union_left hu.symm).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru