Ordered finite-set enumeration and filtering

Main results

• Finset.sort_eq_filter_finRange: a level set in increasing order is the filtered level list.
• Finset.ofFn_orderEmbOfFin: values at its ordered positions form its sorted mapped list.

theorem Finset.sort_eq_filter_finRange {L : ℕ} (s : Finset (Fin L)) : (s.sort fun (a b : Fin L) => a ≤ b) = List.filter (fun (i : Fin L) => decide (i ∈ s)) (List.finRange L)

Increasing level-set enumeration is ordinary filtering of all levels.

theorem Finset.ofFn_orderEmbOfFin {α : Type u_1} {β : Type u_2} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (f : α → β) : (List.ofFn fun (i : Fin k) => f ((s.orderEmbOfFin h) i)) = List.map f (s.sort fun (a b : α) => a ≤ b)

Applying a function to the ordered finite-set positions agrees with its sorted list.