Order isomorphisms from Fin to finsets

We define order isomorphisms like Fin.orderIsoTriple from Fin 3 to the finset {a, b, c} when a < b and b < c.

Future works

• Do the same for Set without too much duplication of code (TODO)
• Provide a definition which would take as an input an order isomorphism e : Fin (n + 1) ≃o s (with s : Set α (or Finset α)) and extend it to an order isomorphism Fin (n + 2) ≃o Finset.insert i s when i < e 0 (TODO).

noncomputable def Fin.orderIsoSingleton {α : Type u_1} [Preorder α] (a : α) : Fin 1 ≃o { x : α // x ∈ {a} }

This is the order isomorphism from Fin 1 to a finset {a}.

Equations

• Fin.orderIsoSingleton a = OrderIso.ofUnique (Fin 1) { x : α // x ∈ {a} }

@[simp]

theorem Fin.orderIsoSingleton_apply {α : Type u_1} [Preorder α] (a : α) (i : Fin 1) : ↑((orderIsoSingleton a) i) = a

noncomputable def Fin.orderIsoPair {α : Type u_1} [Preorder α] [DecidableEq α] (a b : α) (hab : a < b) : Fin 2 ≃o { x : α // x ∈ {a, b} }

This is the order isomorphism from Fin 2 to a finset {a, b} when a < b.

Equations

• Fin.orderIsoPair a b hab = StrictMono.orderIsoOfSurjective ![⟨a, ⋯⟩, ⟨b, ⋯⟩] ⋯ ⋯

@[simp]

theorem Fin.orderIsoPair_zero {α : Type u_1} [Preorder α] [DecidableEq α] (a b : α) (hab : a < b) : ↑((orderIsoPair a b hab) 0) = a

@[simp]

theorem Fin.orderIsoPair_one {α : Type u_1} [Preorder α] [DecidableEq α] (a b : α) (hab : a < b) : ↑((orderIsoPair a b hab) 1) = b

noncomputable def Fin.orderIsoTriple {α : Type u_1} [Preorder α] [DecidableEq α] (a b c : α) (hab : a < b) (hbc : b < c) : Fin 3 ≃o { x : α // x ∈ {a, b, c} }

This is the order isomorphism from Fin 3 to a finset {a, b, c} when a < b and b < c.

Equations

• Fin.orderIsoTriple a b c hab hbc = StrictMono.orderIsoOfSurjective ![⟨a, ⋯⟩, ⟨b, ⋯⟩, ⟨c, ⋯⟩] ⋯ ⋯

@[simp]

theorem Fin.orderIsoTriple_zero {α : Type u_1} [Preorder α] [DecidableEq α] (a b c : α) (hab : a < b) (hbc : b < c) : ↑((orderIsoTriple a b c hab hbc) 0) = a

@[simp]

theorem Fin.orderIsoTriple_one {α : Type u_1} [Preorder α] [DecidableEq α] (a b c : α) (hab : a < b) (hbc : b < c) : ↑((orderIsoTriple a b c hab hbc) 1) = b

@[simp]

theorem Fin.orderIsoTriple_two {α : Type u_1} [Preorder α] [DecidableEq α] (a b c : α) (hab : a < b) (hbc : b < c) : ↑((orderIsoTriple a b c hab hbc) 2) = c