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 #
ofFinEmbEquivis the equivalence betweenFin n ↪o IandSet.powersetCard I nwhenIis a linearly ordered type.
The isomorphism of OrderEmbeddings from Fin n into I with Set.powersetCard I n
when I is linearly ordered.
Instances For
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
{n : ℕ}
{I : Type u_2}
[LinearOrder I]
(s : ↑(powersetCard I n))
:
The natural enumeration of the elements of linearly-ordered type.
Instances For
@[simp]
theorem
Set.powersetCard.orderIsoOfFin_symm_apply_val
{n : ℕ}
{I : Type u_2}
[LinearOrder I]
(s : ↑(powersetCard I n))
(a✝ : ↥↑s)
:
↑((RelIso.symm (orderIsoOfFin s)) a✝) = List.idxOf (↑((OrderIso.setCongr {x : I | x ∈ (↑s).sort fun (x1 x2 : I) => x1 ≤ x2} ↑s ⋯).symm a✝))
((↑s).sort fun (a b : I) => a ≤ b)
@[simp]
theorem
Set.powersetCard.orderIsoOfFin_apply_coe
{n : ℕ}
{I : Type u_2}
[LinearOrder I]
(s : ↑(powersetCard I n))
(a✝ : Fin n)
:
↑((orderIsoOfFin s) a✝) = ((↑s).sort fun (a b : I) => a ≤ b)[↑a✝]
def
Set.powersetCard.permOfDisjoint
{m n : ℕ}
{I : Type u_2}
[LinearOrder I]
{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ₙ.