mk_pi — Mathlib

English

The cardinality of the dependent product Π i, α(i) equals the product of the cardinalities of α(i): # (Π i, α i) = ∏ i, # (α i).

Русский

Кардинал зависимого произведения Π_i α(i) равен произведению кардиналов множеств α(i).

LaTeX

$$$ \#\left(\prod_{i: \iota} \alpha(i)\right) = \prod_{i: \iota} \#(\alpha(i)) $$$

Lean4

@[simp]
theorem mk_pi {ι : Type u} (α : ι → Type v) : #(Π i, α i) = prod fun i => #(α i) :=
  mk_congr <| Equiv.piCongrRight fun _ => outMkEquiv.symm

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