union

Mathlib.Topology.Constructible

URI: https://scilib.ai/kg/mathlib#Topology.IsConstructible.union

English

If s and t are constructible, then s ∪ t is constructible.

Русский

Если s и t конструктивны, то их объединение s ∪ t конструктивно.

LaTeX

$$IsConstructible s → IsConstructible t → IsConstructible (s ∪ t)$$

Lean4

theorem union : IsConstructible s → IsConstructible t → IsConstructible (s ∪ t) :=
  BooleanSubalgebra.sup_mem

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

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

Разделы

Аффилиация

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