Finite order homomorphisms.

The fundamental order homomorphisms between Fin (n + 1) and Fin n.

• Fin.succAbove p i : succAbove p i embeds Fin n into Fin (n + 1) with a hole around p.
• Fin.succAboveEmb p : Fin.succAbove p as an OrderEmbedding.
• Fin.predAbove p i : surjects i : Fin (n+1) into Fin n by subtracting one if p < i.

def Fin.succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : Fin (n + 1)

succAbove p i embeds Fin n into Fin (n + 1) with a hole around p.

Equations

• p.succAbove i = if i.castSucc < p then i.castSucc else i.succ

theorem Fin.succAbove_of_castSucc_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : i.castSucc < p) : p.succAbove i = i.castSucc

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) embeds i by castSucc when the resulting i.castSucc < p.

theorem Fin.succAbove_of_succ_le {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : i.succ ≤ p) : p.succAbove i = i.castSucc

theorem Fin.succAbove_of_le_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p ≤ i.castSucc) : p.succAbove i = i.succ

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) embeds i by succ when the resulting p < i.succ.

theorem Fin.succAbove_of_lt_succ {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p < i.succ) : p.succAbove i = i.succ

theorem Fin.succAbove_succ_of_lt {n : ℕ} (p : Fin n) (i : Fin n) (h : p < i) : p.succ.succAbove i = i.succ

theorem Fin.succAbove_succ_of_le {n : ℕ} (p : Fin n) (i : Fin n) (h : i ≤ p) : p.succ.succAbove i = i.castSucc

@[simp]

theorem Fin.succAbove_succ_self {n : ℕ} (j : Fin n) : j.succ.succAbove j = j.castSucc

theorem Fin.succAbove_castSucc_of_lt {n : ℕ} (p : Fin n) (i : Fin n) (h : i < p) : p.castSucc.succAbove i = i.castSucc

theorem Fin.succAbove_castSucc_of_le {n : ℕ} (p : Fin n) (i : Fin n) (h : p ≤ i) : p.castSucc.succAbove i = i.succ

@[simp]

theorem Fin.succAbove_castSucc_self {n : ℕ} (j : Fin n) : j.castSucc.succAbove j = j.succ

theorem Fin.succAbove_pred_of_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p < i) (hi : optParam (i ≠ 0) ⋯) : p.succAbove (i.pred hi) = i

theorem Fin.succAbove_pred_of_le {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i ≤ p) (hi : i ≠ 0) : p.succAbove (i.pred hi) = (i.pred hi).castSucc

@[simp]

theorem Fin.succAbove_pred_self {n : ℕ} (p : Fin (n + 1)) (h : p ≠ 0) : p.succAbove (p.pred h) = (p.pred h).castSucc

theorem Fin.succAbove_castPred_of_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i < p) (hi : optParam (i ≠ Fin.last n) ⋯) : p.succAbove (i.castPred hi) = i

theorem Fin.succAbove_castPred_of_le {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p ≤ i) (hi : i ≠ Fin.last n) : p.succAbove (i.castPred hi) = (i.castPred hi).succ

theorem Fin.succAbove_castPred_self {n : ℕ} (p : Fin (n + 1)) (h : p ≠ Fin.last n) : p.succAbove (p.castPred h) = (p.castPred h).succ

theorem Fin.succAbove_rev_left {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.rev.succAbove i = (p.succAbove i.rev).rev

theorem Fin.succAbove_rev_right {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i.rev = (p.rev.succAbove i).rev

theorem Fin.succAbove_ne {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i ≠ p

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) never results in p itself

theorem Fin.ne_succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p ≠ p.succAbove i

theorem Fin.strictMono_succAbove {n : ℕ} (p : Fin (n + 1)) : StrictMono p.succAbove

theorem Fin.succAbove_right_injective {n : ℕ} {x : Fin (n + 1)} : Function.Injective x.succAbove

Given a fixed pivot x : Fin (n + 1), x.succAbove is injective

theorem Fin.succAbove_right_inj {n : ℕ} {i : Fin n} {j : Fin n} (x : Fin (n + 1)) : x.succAbove i = x.succAbove j ↔ i = j

Given a fixed pivot x : Fin (n + 1), x.succAbove is injective

theorem Fin.succAbove_lt_succAbove_iff {n : ℕ} {i : Fin n} {j : Fin n} (p : Fin (n + 1)) : p.succAbove i < p.succAbove j ↔ i < j

theorem Fin.succAbove_le_succAbove_iff {n : ℕ} {i : Fin n} {j : Fin n} (p : Fin (n + 1)) : p.succAbove i ≤ p.succAbove j ↔ i ≤ j

@[simp]

theorem Fin.succAboveEmb_toEmbedding {n : ℕ} (p : Fin (n + 1)) : p.succAboveEmb.toEmbedding = { toFun := p.succAbove, inj' := ⋯ }

@[simp]

theorem Fin.succAboveEmb_apply {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAboveEmb i = p.succAbove i

def Fin.succAboveEmb {n : ℕ} (p : Fin (n + 1)) : Fin n ↪o Fin (n + 1)

Fin.succAbove p as an OrderEmbedding.

Equations

• p.succAboveEmb = OrderEmbedding.ofStrictMono p.succAbove ⋯

@[simp]

theorem Fin.succAbove_ne_zero_zero {n : ℕ} [NeZero n] {a : Fin (n + 1)} (ha : a ≠ 0) : a.succAbove 0 = 0

theorem Fin.succAbove_eq_zero_iff {n : ℕ} [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) : a.succAbove b = 0 ↔ b = 0

theorem Fin.succAbove_ne_zero {n : ℕ} [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) (hb : b ≠ 0) : a.succAbove b ≠ 0

@[simp]

theorem Fin.succAbove_zero {n : ℕ} : Fin.succAbove 0 = Fin.succ

Embedding Fin n into Fin (n + 1) with a hole around zero embeds by succ.

theorem Fin.succAbove_zero_apply {n : ℕ} (i : Fin n) : Fin.succAbove 0 i = i.succ

@[simp]

theorem Fin.succAbove_ne_last_last {n : ℕ} {a : Fin (n + 2)} (h : a ≠ Fin.last (n + 1)) : a.succAbove (Fin.last n) = Fin.last (n + 1)

theorem Fin.succAbove_eq_last_iff {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ Fin.last (n + 1)) : a.succAbove b = Fin.last (n + 1) ↔ b = Fin.last n

theorem Fin.succAbove_ne_last {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ Fin.last (n + 1)) (hb : b ≠ Fin.last n) : a.succAbove b ≠ Fin.last (n + 1)

@[simp]

theorem Fin.succAbove_last {n : ℕ} : (Fin.last n).succAbove = Fin.castSucc

Embedding Fin n into Fin (n + 1) with a hole around last n embeds by castSucc.

theorem Fin.succAbove_last_apply {n : ℕ} (i : Fin n) : (Fin.last n).succAbove i = i.castSucc

@[deprecated]

theorem Fin.succAbove_lt_ge {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : i.castSucc < p ∨ p ≤ i.castSucc

@[deprecated Fin.castSucc_lt_or_lt_succ]

theorem Fin.succAbove_lt_gt {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : i.castSucc < p ∨ p < i.succ

Alias of Fin.castSucc_lt_or_lt_succ.

theorem Fin.succAbove_lt_iff_castSucc_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i < p ↔ i.castSucc < p

Embedding i : Fin n into Fin (n + 1) using a pivot p that is greater results in a value that is less than p.

theorem Fin.succAbove_lt_iff_succ_le {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i < p ↔ i.succ ≤ p

theorem Fin.lt_succAbove_iff_le_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p < p.succAbove i ↔ p ≤ i.castSucc

Embedding i : Fin n into Fin (n + 1) using a pivot p that is lesser results in a value that is greater than p.

theorem Fin.lt_succAbove_iff_lt_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p < p.succAbove i ↔ p < i.succ

theorem Fin.succAbove_pos {n : ℕ} [NeZero n] (p : Fin (n + 1)) (i : Fin n) (h : 0 < i) : 0 < p.succAbove i

Embedding a positive Fin n results in a positive Fin (n + 1)

theorem Fin.castPred_succAbove {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : x.castSucc < y) (h' : optParam (y.succAbove x ≠ Fin.last n) ⋯) : (y.succAbove x).castPred h' = x

theorem Fin.pred_succAbove {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : y ≤ x.castSucc) (h' : optParam (y.succAbove x ≠ 0) ⋯) : (y.succAbove x).pred h' = x

theorem Fin.exists_succAbove_eq {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x ≠ y) : ∃ (z : Fin n), y.succAbove z = x

@[simp]

theorem Fin.exists_succAbove_eq_iff {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} : (∃ (z : Fin n), x.succAbove z = y) ↔ y ≠ x

@[simp]

theorem Fin.range_succAbove {n : ℕ} (p : Fin (n + 1)) : Set.range p.succAbove = {p}ᶜ

The range of p.succAbove is everything except p.

@[simp]

theorem Fin.range_succ (n : ℕ) : Set.range Fin.succ = {0}ᶜ

theorem Fin.succAbove_left_injective {n : ℕ} : Function.Injective Fin.succAbove

succAbove is injective at the pivot

@[simp]

theorem Fin.succAbove_left_inj {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} : x.succAbove = y.succAbove ↔ x = y

succAbove is injective at the pivot

@[simp]

theorem Fin.zero_succAbove {n : ℕ} (i : Fin n) : Fin.succAbove 0 i = i.succ

@[simp]

theorem Fin.succ_succAbove_zero {n : ℕ} [NeZero n] (i : Fin n) : i.succ.succAbove 0 = 0

@[simp]

theorem Fin.succ_succAbove_succ {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : i.succ.succAbove j.succ = (i.succAbove j).succ

succ commutes with succAbove.

@[simp]

theorem Fin.castSucc_succAbove_castSucc {n : ℕ} {i : Fin (n + 1)} {j : Fin n} : i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

castSucc commutes with succAbove.

theorem Fin.pred_succAbove_pred {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ 0) (hk : optParam (a.succAbove b ≠ 0) ⋯) : (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

pred commutes with succAbove.

theorem Fin.castPred_succAbove_castPred {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ Fin.last (n + 1)) (hb : b ≠ Fin.last n) (hk : optParam (a.succAbove b ≠ Fin.last (n + 1)) ⋯) : (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

castPred commutes with succAbove.

theorem Fin.rev_succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : (p.succAbove i).rev = p.rev.succAbove i.rev

rev commutes with succAbove.

theorem Fin.one_succAbove_zero {n : ℕ} : Fin.succAbove 1 0 = 0

@[simp]

theorem Fin.succ_succAbove_one {n : ℕ} [NeZero n] (i : Fin (n + 1)) : i.succ.succAbove 1 = (i.succAbove 0).succ

By moving succ to the outside of this expression, we create opportunities for further simplification using succAbove_zero or succ_succAbove_zero.

@[simp]

theorem Fin.one_succAbove_succ {n : ℕ} (j : Fin n) : Fin.succAbove 1 j.succ = j.succ.succ

@[simp]

theorem Fin.one_succAbove_one {n : ℕ} : Fin.succAbove 1 1 = 2

def Fin.predAbove {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : Fin n

predAbove p i surjects i : Fin (n+1) into Fin n by subtracting one if p < i.

Equations

• p.predAbove i = if h : p.castSucc < i then i.pred ⋯ else i.castPred ⋯

theorem Fin.predAbove_of_le_castSucc {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i ≤ p.castSucc) (hi : optParam (i ≠ Fin.last n) ⋯) : p.predAbove i = i.castPred hi

theorem Fin.predAbove_of_lt_succ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i < p.succ) (hi : optParam (i ≠ Fin.last n) ⋯) : p.predAbove i = i.castPred hi

theorem Fin.predAbove_of_castSucc_lt {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.castSucc < i) (hi : optParam (i ≠ 0) ⋯) : p.predAbove i = i.pred hi

theorem Fin.predAbove_of_succ_le {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.succ ≤ i) (hi : optParam (i ≠ 0) ⋯) : p.predAbove i = i.pred hi

theorem Fin.predAbove_succ_of_lt {n : ℕ} (p : Fin n) (i : Fin n) (h : i < p) (hi : optParam (i.succ ≠ Fin.last n) ⋯) : p.predAbove i.succ = i.succ.castPred hi

theorem Fin.predAbove_succ_of_le {n : ℕ} (p : Fin n) (i : Fin n) (h : p ≤ i) : p.predAbove i.succ = i

@[simp]

theorem Fin.predAbove_succ_self {n : ℕ} (p : Fin n) : p.predAbove p.succ = p

theorem Fin.predAbove_castSucc_of_lt {n : ℕ} (p : Fin n) (i : Fin n) (h : p < i) (hi : optParam (i.castSucc ≠ 0) ⋯) : p.predAbove i.castSucc = i.castSucc.pred hi

theorem Fin.predAbove_castSucc_of_le {n : ℕ} (p : Fin n) (i : Fin n) (h : i ≤ p) : p.predAbove i.castSucc = i

@[simp]

theorem Fin.predAbove_castSucc_self {n : ℕ} (p : Fin n) : p.predAbove p.castSucc = p

theorem Fin.predAbove_pred_of_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i < p) (hp : optParam (p ≠ 0) ⋯) (hi : optParam (i ≠ Fin.last n) ⋯) : (p.pred hp).predAbove i = i.castPred hi

theorem Fin.predAbove_pred_of_le {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p ≤ i) (hp : p ≠ 0) (hi : optParam (i ≠ 0) ⋯) : (p.pred hp).predAbove i = i.pred hi

theorem Fin.predAbove_pred_self {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ 0) : (p.pred hp).predAbove p = p.pred hp

theorem Fin.predAbove_castPred_of_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p < i) (hp : optParam (p ≠ Fin.last n) ⋯) (hi : optParam (i ≠ 0) ⋯) : (p.castPred hp).predAbove i = i.pred hi

theorem Fin.predAbove_castPred_of_le {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i ≤ p) (hp : p ≠ Fin.last n) (hi : optParam (i ≠ ⊤) ⋯) : (p.castPred hp).predAbove i = i.castPred hi

theorem Fin.predAbove_castPred_self {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ Fin.last n) : (p.castPred hp).predAbove p = p.castPred hp

theorem Fin.predAbove_rev_left {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : p.rev.predAbove i = (p.predAbove i.rev).rev

theorem Fin.predAbove_rev_right {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : p.predAbove i.rev = (p.rev.predAbove i).rev

@[simp]

theorem Fin.predAbove_right_zero {n : ℕ} [NeZero n] {i : Fin n} : i.predAbove 0 = 0

@[simp]

theorem Fin.predAbove_zero_succ {n : ℕ} [NeZero n] {i : Fin n} : Fin.predAbove 0 i.succ = i

@[simp]

theorem Fin.succ_predAbove_zero {n : ℕ} [NeZero n] {j : Fin (n + 1)} (h : j ≠ 0) : (Fin.predAbove 0 j).succ = j

@[simp]

theorem Fin.predAbove_zero_of_ne_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} (hi : i ≠ 0) : Fin.predAbove 0 i = i.pred hi

theorem Fin.predAbove_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} : Fin.predAbove 0 i = if hi : i = 0 then 0 else i.pred hi

@[simp]

theorem Fin.predAbove_right_last {n : ℕ} {i : Fin (n + 1)} : i.predAbove (Fin.last (n + 1)) = Fin.last n

@[simp]

theorem Fin.predAbove_last_castSucc {n : ℕ} {i : Fin (n + 1)} : (Fin.last n).predAbove i.castSucc = i

@[simp]

theorem Fin.predAbove_last_of_ne_last {n : ℕ} {i : Fin (n + 2)} (hi : i ≠ Fin.last (n + 1)) : (Fin.last n).predAbove i = i.castPred hi

theorem Fin.predAbove_last_apply {n : ℕ} {i : Fin (n + 2)} : (Fin.last n).predAbove i = if hi : i = Fin.last (n + 1) then Fin.last n else i.castPred hi

theorem Fin.predAbove_right_monotone {n : ℕ} (p : Fin n) : Monotone p.predAbove

theorem Fin.predAbove_left_monotone {n : ℕ} (i : Fin (n + 1)) : Monotone fun (p : Fin n) => p.predAbove i

@[simp]

theorem Fin.predAboveOrderHom_coe {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : p.predAboveOrderHom i = p.predAbove i

def Fin.predAboveOrderHom {n : ℕ} (p : Fin n) : Fin (n + 1) →o Fin n

Fin.predAbove p as an OrderHom.

Equations

• p.predAboveOrderHom = { toFun := p.predAbove, monotone' := ⋯ }

@[simp]

theorem Fin.succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.castSucc) : p.castSucc.succAbove (p.predAbove i) = i

Sending Fin (n+1) to Fin n by subtracting one from anything above p then back to Fin (n+1) with a gap around p is the identity away from p.

@[simp]

theorem Fin.predAbove_succAbove {n : ℕ} (p : Fin n) (i : Fin n) : p.predAbove (p.castSucc.succAbove i) = i

Sending Fin n into Fin (n + 1) with a gap at p then back to Fin n by subtracting one from anything above p is the identity.

@[simp]

theorem Fin.succ_predAbove_succ {n : ℕ} (a : Fin n) (b : Fin (n + 1)) : a.succ.predAbove b.succ = (a.predAbove b).succ

succ commutes with predAbove.

@[simp]

theorem Fin.castSucc_predAbove_castSucc {n : ℕ} (a : Fin n) (b : Fin (n + 1)) : a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

castSucc commutes with predAbove.

theorem Fin.rev_predAbove {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : (p.predAbove i).rev = p.rev.predAbove i.rev

rev commutes with predAbove.