inter

Mathlib.Topology.Constructible

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

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 inter : IsConstructible s → IsConstructible t → IsConstructible (s ∩ t) :=
  BooleanSubalgebra.inf_mem

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

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

Разделы

Аффилиация

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