small_biInter — Mathlib

English

The double-indexed intersection over i and hi is small when each f(i, hi) is small.

Русский

Двойное пересечение по i и hi малое, если каждое f(i, hi) мало.

LaTeX

$$$\forall (i : ι) (hi : i \in s), \operatorname{Small}(f(i, hi)) \Rightarrow \operatorname{Small}(\bigcap_{i} \bigcap_{hi} f(i, hi))$$$

Lean4

theorem small_biInter {s : Set ι} {i : ι} (hi : i ∈ s) (f : (i : ι) → i ∈ s → Set α) [Small.{u} (f i hi)] :
    Small.{u} (⋂ i, ⋂ hi, f i hi) :=
  Set.biInter_eq_iInter s f ▸ small_iInter _ ⟨i, hi⟩

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