Finite sets of an ordered type

This file defines the isomorphism between ordered embeddings into a linearly ordered type and the finite sets of that type.

Definitions

• ofFinEmbEquiv is the equivalence between Fin n ↪o I and Set.powersetCard I n when I is a linearly ordered type.

def Set.powersetCard.ofFinEmbEquiv {n : ℕ} {I : Type u_1} [LinearOrder I] : Fin n ↪o I ≃ ↑(powersetCard I n)

The isomorphism of OrderEmbeddings from Fin n into I with Set.powersetCard I n when I is linearly ordered.

Equations

• One or more equations did not get rendered due to their size.

theorem Set.powersetCard.ofFinEmbEquiv_apply {n : ℕ} {I : Type u_1} [LinearOrder I] (f : Fin n ↪o I) : ofFinEmbEquiv f = ofFinEmb n I f.toEmbedding

theorem Set.powersetCard.ofFinEmbEquiv_symm_apply {n : ℕ} {I : Type u_1} [LinearOrder I] (s : ↑(powersetCard I n)) : ofFinEmbEquiv.symm s = (↑s).orderEmbOfFin ⋯

@[simp]

theorem Set.powersetCard.mem_ofFinEmbEquiv_iff_mem_range {n : ℕ} {I : Type u_1} [LinearOrder I] (f : Fin n ↪o I) (i : I) : i ∈ ofFinEmbEquiv f ↔ i ∈ range ⇑f

theorem Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem {n : ℕ} {I : Type u_1} [LinearOrder I] (s : ↑(powersetCard I n)) (i : I) : i ∈ range ⇑(ofFinEmbEquiv.symm s) ↔ i ∈ s

def Set.powersetCard.orderIsoOfFin {I : Type u_1} [LinearOrder I] {n : ℕ} (s : ↑(powersetCard I n)) : Fin n ≃o ↥↑s

The natural enumeration of the elements of linearly-ordered type.

Equations

• Set.powersetCard.orderIsoOfFin s = (↑s).orderIsoOfFin ⋯

@[simp]

theorem Set.powersetCard.orderIsoOfFin_symm_apply_val {I : Type u_1} [LinearOrder I] {n : ℕ} (s : ↑(powersetCard I n)) (a✝ : ↥↑s) : ↑((RelIso.symm (orderIsoOfFin s)) a✝) = List.idxOf (↑(({x : I | x ∈ (↑s).sort fun (x1 x2 : I) => x1 ≤ x2}.orderIsoOfEq ↑s ⋯).symm a✝)) ((↑s).sort fun (a b : I) => a ≤ b)

@[simp]

theorem Set.powersetCard.orderIsoOfFin_apply_coe {I : Type u_1} [LinearOrder I] {n : ℕ} (s : ↑(powersetCard I n)) (a✝ : Fin n) : ↑((orderIsoOfFin s) a✝) = ((↑s).sort fun (a b : I) => a ≤ b)[↑a✝]

def Set.powersetCard.permOfDisjoint {I : Type u_1} [LinearOrder I] {m n : ℕ} {s : ↑(powersetCard I m)} {t : ↑(powersetCard I n)} (h : Disjoint ↑s ↑t) : Equiv.Perm (Fin (m + n))

The permutation of Fin (m + n) corresponding to adjoining a Finset of card m to a Finset of card n and sorting the resulting set. In other words, given s₁ < s₂ < ⋯ < sₘ and t₁ < t₂ < ⋯ < tₙ (disjoint) this is the permutation obtained by sorting s₁, s₂, …, sₘ, t₁, t₂, …, tₙ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Set.powersetCard.sign {n : ℕ} {I : Type u_1} [LinearOrder I] [Fintype I] (s : ↑(powersetCard I n)) : ℤˣ

A subset s of a linearly-ordered finite type I, determines a permutation of I by moving all these terms of s to the front. This is the sign of that permutation.

Equations

• Set.powersetCard.sign s = Equiv.Perm.sign (Set.powersetCard.permOfDisjoint ⋯)

theorem Set.powersetCard.sign_eq_permOfDisjoint_sign {n : ℕ} {I : Type u_1} [LinearOrder I] [Fintype I] {m : ℕ} (hkl : n + m = Fintype.card I) (s : ↑(powersetCard I n)) (t : ↑(powersetCard I m)) (hst : Disjoint ↑s ↑t) : powersetCard.sign s = Equiv.Perm.sign (permOfDisjoint hst)