English
Let ι be a type and a a cardinal. The sum over ι of a constant a has cardinality lift(#ι) · lift(a): ∑_{i:ι} a = lift(|ι|) · lift(a).
Русский
Пусть ι — тип, a — кардинал. Сумма константы a по i из ι имеет кардинал равный lift(|ι|) · lift(a).
LaTeX
$$$\Big(\sum _{i : \iota} a\Big) = \operatorname{lift}(\#\iota) \cdot \operatorname{lift}(a)$$$
Lean4
@[simp]
theorem sum_const (ι : Type u) (a : Cardinal.{v}) : (sum fun _ : ι => a) = lift.{v} #ι * lift.{u} a :=
inductionOn a fun α =>
mk_congr <|
calc
(Σ _ : ι, Quotient.out #α) ≃ ι × Quotient.out #α := Equiv.sigmaEquivProd _ _
_ ≃ ULift ι × ULift α := Equiv.ulift.symm.prodCongr (outMkEquiv.trans Equiv.ulift.symm)
