small_biInter' — Mathlib

English

If s is nonempty and every t ∈ s is small, then ⋂ i ∈ s t(i) is small.

Русский

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

LaTeX

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

Lean4

instance small_biInter' (s : Set ι) [Nonempty s] (f : (i : ι) → i ∈ s → Set α) [∀ i hi, Small.{u} (f i hi)] :
    Small.{u} (⋂ i, ⋂ hi, f i hi) :=
  let ⟨t⟩ : Nonempty s := inferInstance
  small_biInter t.prop f

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