small_sigma — Mathlib

English

If α is Small and each β(a) is Small, then the dependent sigma-type Σa:α, β(a) is Small.

Русский

Если α мала и для каждого a ∈ α β(a) мала, то зависимый сигма-тип Σa:α, β(a) мал.

LaTeX

$$$Small(\alpha) \land (\forall a:\alpha, Small(\beta(a))) \Rightarrow Small\left(\sum_{a:\alpha} \beta(a)\right).$$$

Lean4

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

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