nnratCast_dens_mul_natCast_card — Mathlib

English

Let α be finite and s ⊆ α a Finset. The density of s, when multiplied by the cardinality of α, equals the cardinality of s.

Русский

Пусть α — конечное множество, и s ⊆ α является конечным подмножеством. Плотность s, умноженная на кардинал α, равна кардиналу s.

LaTeX

$$$ (\\operatorname{dens}(s) \\cdot \\operatorname{card}(\\alpha) : \\mathbb{𝕜}) = \\operatorname{card}(s) $$$

Lean4

@[simp]
theorem nnratCast_dens_mul_natCast_card (s : Finset α) : (s.dens * Fintype.card α : 𝕜) = s.card :=
  mod_cast s.dens_mul_card

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