small_iInter

Mathlib.Logic.Small.Set

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

English

The meet over i of s(i) is small if each s(i) is small.

Русский

Пересечение по индексу i: ⋂ i, s(i) малое, если каждое s(i) мало.

LaTeX

$$$\forall i, \operatorname{Small}(s(i)) \Rightarrow \operatorname{Small}(\bigcap_{i} s(i))$$$

Lean4

theorem small_iInter (s : ι → Set α) (i : ι) [Small.{u} (s i)] : Small.{u} (⋂ i, s i) :=
  small_subset (Set.iInter_subset s i)

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

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

Разделы

Аффилиация

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