generateFrom_iUnion

Mathlib.Topology.Order

URI: https://scilib.ai/kg/mathlib#generateFrom_iUnion

English

Let f : ι → Set(Set α). Then generateFrom(⋃ i, f i) = ⨅ i, generateFrom(f i).

Русский

Пусть f : ι → Set(Set α). Тогда generateFrom(⋃ i, f i) = ⨅ i, generateFrom(f i).

LaTeX

$$$\\operatorname{generateFrom}\\left(\\bigcup_i f(i)\\right) = \\bigwedge_i \\operatorname{generateFrom}(f(i))$$$

Lean4

theorem generateFrom_iUnion {f : ι → Set (Set α)} : generateFrom (⋃ i, f i) = ⨅ i, generateFrom (f i) :=
  (gc_generateFrom α).u_iInf

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

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

Разделы

Аффилиация

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