count_apply_finite — Mathlib

English

Let s be a finite subset of a type α. Then count s equals the cardinality of s as a finset.

Русский

Пусть s — конечное подмножество множества α. Тогда count s равно кардиналу множества s, выраженному через конечный подмножество.

LaTeX

$$$count\;s = (s.Finite.toFinset.card).cast$$$

Lean4

theorem count_apply_finite [MeasurableSingletonClass α] (s : Set α) (hs : s.Finite) : count s = #hs.toFinset := by
  rw [← count_apply_finset, Finite.coe_toFinset]

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