sdiff

Mathlib.Topology.Constructible

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

English

If s and t are constructible, then the set difference s \\ t is constructible.

Русский

Если s и t конструктивны, то множество различия s \\ t конструктивно.

LaTeX

$$IsConstructible s → IsConstructible t → IsConstructible (s \\ t)$$

Lean4

theorem sdiff : IsConstructible s → IsConstructible t → IsConstructible (s \ t) :=
  BooleanSubalgebra.sdiff_mem

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

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

Разделы

Аффилиация

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