card_mk — Mathlib

English

For a Multiset m with nodup, the cardinality of the Finset ⟨m, nodup⟩ equals the cardinality of m: #⟨m, nodup⟩ = Multiset.card m.

Русский

Для мультисета m с nodup кардинальность финсета ⟨m, nodup⟩ равна кардинальности m.

LaTeX

$$$\#(⟨m,\text{nodup}\rangle : Finset \alpha) = \operatorname{Multiset.card} m$$$

Lean4

@[simp]
theorem card_mk {m nodup} : #(⟨m, nodup⟩ : Finset α) = Multiset.card m :=
  rfl

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