Theorems · Definition · combinatorics

finSumEquivOfFinset

{α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] → [LinearOrder α] → {m n : ℕ} → {s : Finset α} → s.card = m → sᶜ.card = n → Fin m ⊕ Fin n ≃ α

If α is a linearly ordered fintype, s : Finset α has cardinality m and its complement has cardinality n, then Fin m ⊕ Fin n ≃ α. The equivalence sends elements of Fin m to elements of s and elements of Fin n to elements of sᶜ while preserving order on each "half" of Fin m ⊕ Fin n (using Set.orderIsoOfFin).

Defined in

Mathlib.Data.Fintype.Sort

Cited by

7 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeLinearOrder