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

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

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

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 : Fin.succ i ≤ p) : Fin.succAbove p i = Fin.castSucc i

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

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 < Fin.succ i) : Fin.succAbove p i = Fin.succ i

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

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

@[simp]

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

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

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

@[simp]

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

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

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

@[simp]

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

theorem Fin.succAbove_castPred_of_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i < p) (hi : optParam (i ≠ Fin.last n) ⋯) : Fin.succAbove p (Fin.castPred i 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) : Fin.succAbove p (Fin.castPred i hi) = Fin.succ (Fin.castPred i hi)

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

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

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

theorem Fin.succAbove_ne {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : Fin.succAbove p 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 ≠ Fin.succAbove p i

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

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

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)) : Fin.succAbove x i = Fin.succAbove x 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)) : Fin.succAbove p i < Fin.succAbove p j ↔ i < j

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

@[simp]

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

@[simp]

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

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

Fin.succAbove p as an OrderEmbedding.

Equations

• Fin.succAboveEmb p = OrderEmbedding.ofStrictMono (Fin.succAbove p) ⋯

@[simp]

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

theorem Fin.succAbove_eq_zero_iff {n : ℕ} [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) : Fin.succAbove a 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) : Fin.succAbove a 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 = Fin.succ i

@[simp]

theorem Fin.succAbove_ne_last_last {n : ℕ} {a : Fin (n + 2)} (h : a ≠ Fin.last (n + 1)) : Fin.succAbove a (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)) : Fin.succAbove a 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) : Fin.succAbove a b ≠ Fin.last (n + 1)

@[simp]

theorem Fin.succAbove_last {n : ℕ} : Fin.succAbove (Fin.last n) = 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.succAbove (Fin.last n) i = Fin.castSucc i

@[deprecated]

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

@[deprecated Fin.castSucc_lt_or_lt_succ]

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

Alias of Fin.castSucc_lt_or_lt_succ.

theorem Fin.succAbove_lt_iff_castSucc_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : Fin.succAbove p i < p ↔ Fin.castSucc i < 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) : Fin.succAbove p i < p ↔ Fin.succ i ≤ p

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

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 < Fin.succAbove p i ↔ p < Fin.succ i

theorem Fin.succAbove_pos {n : ℕ} [NeZero n] (p : Fin (n + 1)) (i : Fin n) (h : 0 < i) : 0 < Fin.succAbove p 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 : Fin.castSucc x < y) (h' : optParam (Fin.succAbove y x ≠ Fin.last n) ⋯) : Fin.castPred (Fin.succAbove y x) h' = x

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

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

@[simp]

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

@[simp]

theorem Fin.range_succAbove {n : ℕ} (p : Fin (n + 1)) : Set.range (Fin.succAbove p) = {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)} : Fin.succAbove x = Fin.succAbove y ↔ x = y

succAbove is injective at the pivot

@[simp]

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

@[simp]

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

@[simp]

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

succ commutes with succAbove.

@[simp]

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

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 (Fin.succAbove a b ≠ 0) ⋯) : Fin.succAbove (Fin.pred a ha) (Fin.pred b hb) = Fin.pred (Fin.succAbove a b) 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 (Fin.succAbove a b ≠ Fin.last (n + 1)) ⋯) : Fin.succAbove (Fin.castPred a ha) (Fin.castPred b hb) = Fin.castPred (Fin.succAbove a b) hk

castPred commutes with succAbove.

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

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)) : Fin.succAbove (Fin.succ i) 1 = Fin.succ (Fin.succAbove i 0)

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 (Fin.succ j) = Fin.succ (Fin.succ j)

@[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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

theorem Fin.predAbove_castSucc_self {n : ℕ} (p : Fin n) : Fin.predAbove p (Fin.castSucc p) = 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) ⋯) : Fin.predAbove (Fin.pred p hp) i = Fin.castPred i 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) ⋯) : Fin.predAbove (Fin.pred p hp) i = Fin.pred i hi

theorem Fin.predAbove_pred_self {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ 0) : Fin.predAbove (Fin.pred p hp) p = Fin.pred p 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) ⋯) : Fin.predAbove (Fin.castPred p hp) i = Fin.pred i 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 ≠ ⊤) ⋯) : Fin.predAbove (Fin.castPred p hp) i = Fin.castPred i hi

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

Fin.predAbove p as an OrderHom.

Equations

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

@[simp]

theorem Fin.succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ Fin.castSucc p) : Fin.succAbove (Fin.castSucc p) (Fin.predAbove p 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) : Fin.predAbove p (Fin.succAbove (Fin.castSucc p) 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)) : Fin.predAbove (Fin.succ a) (Fin.succ b) = Fin.succ (Fin.predAbove a b)

succ commutes with predAbove.

@[simp]

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

castSucc commutes with predAbove.

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

rev commutes with predAbove.