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.

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