sort_univ — Mathlib

English

The univ Finset, sorted by the natural order, equals the canonical list 0,1,...,n−1.

Русский

Объединённое множество (univ) упорядочено по естественному порядку и даёт канонический список 0,1,...,n−1.

LaTeX

$$Finset.univ.sort (\,) = List.finRange n$$

Lean4

theorem sort_univ (n : ℕ) : Finset.univ.sort (fun x y : Fin n => x ≤ y) = List.finRange n :=
  List.eq_of_perm_of_sorted
    (List.perm_of_nodup_nodup_toFinset_eq (Finset.univ.sort_nodup _) (List.nodup_finRange n) (by simp))
    (Finset.univ.sort_sorted LE.le) (List.pairwise_le_finRange n)

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