small_Pi — Mathlib

English

If α is small and β(a) is small for every a, then the dependent function type ∀ a: α, β(a) is small.

Русский

Если α мала и для каждого a: α β(a) мала, то зависимая функция ∀ a: α, β(a) мала.

LaTeX

$$$ \\text{Small}(\\prod_{a:\\alpha} \\beta(a)) $$$

Lean4

instance small_Pi {α} (β : α → Type*) [Small.{w} α] [∀ a, Small.{w} (β a)] : Small.{w} (∀ a, β a) :=
  ⟨⟨∀ a' : Shrink α, Shrink (β ((equivShrink α).symm a')),
      ⟨Equiv.piCongr (equivShrink α) fun a => by simpa using equivShrink (β a)⟩⟩⟩

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