finite_iInter — Mathlib

English

If ι is a nonempty index set and t i are sets for each i with each t i finite, then the intersection ⋂ i, t i is finite.

Русский

Если множество индексов ι непусто и для каждого i множество t i, причём все t i конечны, то пересечение ⋂ i t i конечно.

LaTeX

$$$\\operatorname{Finite}\\left(\\bigcap_{i} t(i)\\right)$$$

Lean4

instance finite_iInter {ι : Sort*} [Nonempty ι] (t : ι → Set α) [∀ i, Finite (t i)] : Finite (⋂ i, t i) :=
  Finite.Set.subset (t <| Classical.arbitrary ι) (iInter_subset _ _)

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