Documentation

CombinatorialRigidity.Mathlib.Data.Finset.Sort

Mirror file: Mathlib/Data/Finset/Sort.lean #

Upstream-eligible lemmas about Finset.orderEmbOfFin. See DESIGN.md Mirror directory for the project convention.

source
@[simp]
theorem Finset.univ_orderEmbOfFin {n : ℕ} (h : univ.card = n) :
⇑(univ.orderEmbOfFin h) = id

The increasing enumeration of Finset.univ : Finset (Fin n) is the identity.

Finset.univ.orderEmbOfFin h is the unique StrictMono map Fin n → Fin n landing in univ, and id is such a map; orderEmbOfFin_unique identifies the two. The cardinality hypothesis h : (univ : Finset (Fin n)).card = n is Finset.card_fin n.