small_setPi — Mathlib

English

If α is Small and each s(a) is Small, then Set.univ.pi s is Small.

Русский

Если α мала и каждый s(a) мала, то Set.univ.pi s мала.

LaTeX

$$$Small(\alpha) \land (\forall a, Small(s(a))) \Rightarrow Small(\mathrm{Set.univ}.pi\, s).$$$

Lean4

instance small_setPi {β : α → Type u2} (s : (a : α) → Set (β a)) [Small.{u} α] [∀ a, Small.{u} (s a)] :
    Small.{u} (Set.pi Set.univ s) :=
  small_of_injective (Equiv.Set.univPi s).injective

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