range_val — Mathlib

English

The underlying multiset of range(n) is exactly Multiset.range(n), i.e., the multiset consisting of 0,1,...,n−1 with appropriate multiplicities.

Русский

Подлежащий диапазону Finset(n) подмножество представлено мультимножеством Multiset.range(n), то есть мультимножеством {0,1,...,n−1}.

LaTeX

$$$$ (\mathrm{range}(n)).\mathrm{val} = \operatorname{Multiset.range}(n). $$$$

Lean4

@[simp]
theorem range_val (n : ℕ) : (range n).1 = Multiset.range n :=
  rfl

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