iUnion

Mathlib.Topology.Constructible

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

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 iUnion [Finite ι] {f : ι → Set X} (hf : ∀ i, IsConstructible (f i)) : IsConstructible (⋃ i, f i) :=
  BooleanSubalgebra.iSup_mem hf

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

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

Разделы

Аффилиация

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