iInter

Mathlib.Topology.Constructible

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

English

If ι is finite and each f(i) is constructible, then ⋂ i, f(i) is constructible.

Русский

Если ι конечен и каждый f(i) конструктивен, то ⋂ i f(i) конструктивно.

LaTeX

$$IsConstructible (⋂ i, f i)$$

Lean4

theorem iInter [Finite ι] {f : ι → Set X} (hf : ∀ i, IsConstructible (f i)) : IsConstructible (⋂ i, f i) :=
  BooleanSubalgebra.iInf_mem hf

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

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

Разделы

Аффилиация

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