mk_sigma — Mathlib

English

The cardinality of the sigma-type Σ i, f i equals the sum of the cardinals |f i| over i: |Σ i, f i| = ∑_i |f i|.

Русский

Кардинал сигма-типа Σ i, f i равен сумме кардиналов величин |f i| по i: |Σ i, f i| = ∑_i |f i|.

LaTeX

$$$|\Sigma i, f i| = \sum_i |f i|$$$

Lean4

@[simp]
theorem mk_sigma {ι} (f : ι → Type*) : #(Σ i, f i) = sum fun i => #(f i) :=
  mk_congr <| Equiv.sigmaCongrRight fun _ => outMkEquiv.symm

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