small_iInter' — Mathlib

English

If ι is nonempty and each s(i) is small, then ⋂ i, s(i) is small.

Русский

Если ι непусто и каждое s(i) мало, тогда ⋂ i, s(i) мало.

LaTeX

$$$[\text{Nonempty } \iota] \; (\forall i, \operatorname{Small}(s(i))) \Rightarrow \operatorname{Small}(\bigcap_{i} s(i))$$$

Lean4

instance small_iInter' [Nonempty ι] (s : ι → Set α) [∀ i, Small.{u} (s i)] : Small.{u} (⋂ i, s i) :=
  let ⟨i⟩ : Nonempty ι := inferInstance
  small_iInter s i

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