# Successors and predecessor operations of `Fin n` #

This file contains a number of definitions and lemmas related to `Fin.succ`, `Fin.pred`, and related operations on `Fin n`.

## Main definitions #

- `finCongr` : `Fin.cast` as an `Equiv`, equivalence between `Fin n` and `Fin m` when `n = m`;
- `Fin.succAbove` : embeds `Fin n` into `Fin (n + 1)` skipping `p`.
- `Fin.predAbove` : the (partial) inverse of `Fin.succAbove`.

### succ and casts into larger Fin types #

source
theorem Fin.succ_injective (n : ℕ) :
Function.Injective succ
source
@[simp]
theorem Fin.exists_succ_eq {n : ℕ} {x : Fin (n + 1)} :
(∃ (y : Fin n), y.succ = x) ↔ x ≠ 0
source
theorem Fin.exists_succ_eq_of_ne_zero {n : ℕ} {x : Fin (n + 1)} (h : x ≠ 0) :
∃ (y : Fin n), y.succ = x
source
@[simp]
theorem Fin.succ_zero_eq_one' {n : ℕ} [NeZero n] :
succ 0 = 1
source
theorem Fin.one_pos' {n : ℕ} [NeZero n] :
0 < 1
source
theorem Fin.zero_ne_one' {n : ℕ} [NeZero n] :
0 ≠ 1
source
@[simp]
theorem Fin.succ_one_eq_two' {n : ℕ} [NeZero n] :
succ 1 = 2

The `Fin.succ_one_eq_two` in `Lean` only applies in `Fin (n+2)`. This one instead uses a `NeZero n` typeclass hypothesis.

source
@[simp]
theorem Fin.le_zero_iff' {n : ℕ} [NeZero n] {k : Fin n} :
k ≤ 0 ↔ k = 0

The `Fin.le_zero_iff` in `Lean` only applies in `Fin (n+1)`. This one instead uses a `NeZero n` typeclass hypothesis.

source
@[simp]
theorem Fin.castLE_inj {n m : ℕ} {hmn : m ≤ n} {a b : Fin m} :
castLE hmn a = castLE hmn b ↔ a = b
source
@[simp]
theorem Fin.castAdd_inj {n m : ℕ} {a b : Fin m} :
castAdd n a = castAdd n b ↔ a = b
source
theorem Fin.castLE_injective {n m : ℕ} (hmn : m ≤ n) :
Function.Injective (castLE hmn)
source
theorem Fin.castAdd_injective (m n : ℕ) :
Function.Injective (castAdd n)
source
theorem Fin.castSucc_injective (n : ℕ) :
Function.Injective castSucc
source
@[simp]
theorem Fin.castLE_castSucc {n m : ℕ} (i : Fin n) (h : n + 1 ≤ m) :
castLE h i.castSucc = castLE ⋯ i
source
@[simp]
theorem Fin.castLE_comp_castSucc {n m : ℕ} (h : n + 1 ≤ m) :
castLE h ∘ castSucc = castLE ⋯
source
@[simp]
theorem Fin.castLE_rfl (n : ℕ) :
castLE ⋯ = id
source
@[simp]
theorem Fin.range_castLE {n k : ℕ} (h : n ≤ k) :
Set.range (castLE h) = {i : Fin k | ↑i < n}
source
@[simp]
theorem Fin.coe_of_injective_castLE_symm {n k : ℕ} (h : n ≤ k) (i : Fin k) (hi : i ∈ Set.range (castLE h)) :
↑((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩) = ↑i
source
theorem Fin.leftInverse_cast {n m : ℕ} (eq : n = m) :
Function.LeftInverse (Fin.cast ⋯) (Fin.cast eq)
source
theorem Fin.rightInverse_cast {n m : ℕ} (eq : n = m) :
Function.RightInverse (Fin.cast ⋯) (Fin.cast eq)
source
@[simp]
theorem Fin.cast_inj {n m : ℕ} (eq : n = m) {a b : Fin n} :
Fin.cast eq a = Fin.cast eq b ↔ a = b
source
@[simp]
theorem Fin.cast_lt_cast {n m : ℕ} (eq : n = m) {a b : Fin n} :
Fin.cast eq a < Fin.cast eq b ↔ a < b
source
@[simp]
theorem Fin.cast_le_cast {n m : ℕ} (eq : n = m) {a b : Fin n} :
Fin.cast eq a ≤ Fin.cast eq b ↔ a ≤ b
source
def finCongr {n m : ℕ} (eq : n = m) :
Fin n ≃ Fin m

The 'identity' equivalence between `Fin m` and `Fin n` when `m = n`.

Equations

- finCongr eq = { toFun := Fin.cast eq, invFun := Fin.cast ⋯, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem finCongr_symm_apply {n m : ℕ} (eq : n = m) (i : Fin m) :
(finCongr eq).symm i = Fin.cast ⋯ i
source
@[simp]
theorem finCongr_apply {n m : ℕ} (eq : n = m) (i : Fin n) :
(finCongr eq) i = Fin.cast eq i
source
@[simp]
theorem finCongr_apply_mk {n m : ℕ} (h : m = n) (k : ℕ) (hk : k < m) :
(finCongr h) ⟨k, hk⟩ = ⟨k, ⋯⟩
source
@[simp]
theorem finCongr_refl {n : ℕ} (h : n = n := ⋯) :
finCongr h = Equiv.refl (Fin n)
source
@[simp]
theorem finCongr_symm {n m : ℕ} (h : m = n) :
(finCongr h).symm = finCongr ⋯
source
@[simp]
theorem finCongr_apply_coe {n m : ℕ} (h : m = n) (k : Fin m) :
↑((finCongr h) k) = ↑k
source
theorem finCongr_symm_apply_coe {n m : ℕ} (h : m = n) (k : Fin n) :
↑((finCongr h).symm k) = ↑k
source
theorem finCongr_eq_equivCast {n m : ℕ} (h : n = m) :
finCongr h = Equiv.cast ⋯

While in many cases `finCongr` is better than `Equiv.cast`/`cast`, sometimes we want to apply a generic theorem about `cast`.

source
theorem Fin.cast_eq_cast {n m : ℕ} (h : n = m) :
Fin.cast h = cast ⋯

While in many cases `Fin.cast` is better than `Equiv.cast`/`cast`, sometimes we want to apply a generic theorem about `cast`.

source
theorem Fin.castSucc_le_succ {n : ℕ} (i : Fin n) :
i.castSucc ≤ i.succ
source
@[simp]
theorem Fin.castSucc_le_castSucc_iff {n : ℕ} {a b : Fin n} :
a.castSucc ≤ b.castSucc ↔ a ≤ b
source
@[simp]
theorem Fin.succ_le_castSucc_iff {n : ℕ} {a b : Fin n} :
a.succ ≤ b.castSucc ↔ a < b
source
@[simp]
theorem Fin.castSucc_lt_succ_iff {n : ℕ} {a b : Fin n} :
a.castSucc < b.succ ↔ a ≤ b
source
theorem Fin.le_of_castSucc_lt_of_succ_lt {n : ℕ} {a b : Fin (n + 1)} {i : Fin n} (hl : i.castSucc < a) (hu : b < i.succ) :
b < a
source
theorem Fin.castSucc_lt_or_lt_succ {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :
i.castSucc < p ∨ p < i.succ
source
theorem Fin.succ_le_or_le_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :
i.succ ≤ p ∨ p ≤ i.castSucc
source
theorem Fin.eq_castSucc_of_ne_last {n : ℕ} {x : Fin (n + 1)} (h : x ≠ last n) :
∃ (y : Fin n), y.castSucc = x
source
theorem Fin.forall_fin_succ' {n : ℕ} {P : Fin (n + 1) → Prop} :
(∀ (i : Fin (n + 1)), P i) ↔ (∀ (i : Fin n), P i.castSucc) ∧ P (last n)
source
theorem Fin.eq_castSucc_or_eq_last {n : ℕ} (i : Fin (n + 1)) :
(∃ (j : Fin n), i = j.castSucc) ∨ i = last n
source
@[simp]
theorem Fin.castSucc_ne_last {n : ℕ} (i : Fin n) :
i.castSucc ≠ last n
source
theorem Fin.exists_fin_succ' {n : ℕ} {P : Fin (n + 1) → Prop} :
(∃ (i : Fin (n + 1)), P i) ↔ (∃ (i : Fin n), P i.castSucc) ∨ P (last n)
source
@[simp]
theorem Fin.castSucc_zero' {n : ℕ} [NeZero n] :
castSucc 0 = 0

The `Fin.castSucc_zero` in `Lean` only applies in `Fin (n+1)`. This one instead uses a `NeZero n` typeclass hypothesis.

source
@[simp]
theorem Fin.castSucc_pos_iff {n : ℕ} [NeZero n] {i : Fin n} :
0 < i.castSucc ↔ 0 < i
source
theorem Fin.castSucc_pos' {n : ℕ} [NeZero n] {i : Fin n} :
0 < i → 0 < i.castSucc

`castSucc i` is positive when `i` is positive.

The `Fin.castSucc_pos` in `Lean` only applies in `Fin (n+1)`. This one instead uses a `NeZero n` typeclass hypothesis.

source
@[deprecated Fin.castSucc_eq_zero_iff (since := "2025-05-13")]
theorem Fin.castSucc_eq_zero_iff' {n : ℕ} [NeZero n] (a : Fin n) :
a.castSucc = 0 ↔ a = 0
source
@[deprecated Fin.castSucc_ne_zero_iff (since := "2025-05-13")]
theorem Fin.castSucc_ne_zero_iff' {n : ℕ} [NeZero n] (a : Fin n) :
a.castSucc ≠ 0 ↔ a ≠ 0
source
theorem Fin.castSucc_ne_zero_of_lt {n : ℕ} {p i : Fin n} (h : p < i) :
i.castSucc ≠ 0
source
theorem Fin.succ_ne_last_iff {n : ℕ} (a : Fin (n + 1)) :
a.succ ≠ last (n + 1) ↔ a ≠ last n
source
theorem Fin.succ_ne_last_of_lt {n : ℕ} {p i : Fin n} (h : i < p) :
i.succ ≠ last n
source
@[simp]
theorem Fin.coe_eq_castSucc {n : ℕ} {a : Fin n} :
↑↑a = a.castSucc
source
theorem Fin.coe_succ_lt_iff_lt {n : ℕ} {j k : Fin n} :
↑↑j < ↑↑k ↔ j < k
source
@[simp]
theorem Fin.range_castSucc {n : ℕ} :
Set.range castSucc = {i : Fin n.succ | ↑i < n}
source
@[simp]
theorem Fin.coe_of_injective_castSucc_symm {n : ℕ} (i : Fin n.succ) (hi : i ∈ Set.range castSucc) :
↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩) = ↑i
source
theorem Fin.castSucc_castAdd {n m : ℕ} (i : Fin n) :
(castAdd m i).castSucc = castAdd (m + 1) i
source
theorem Fin.succ_castAdd {n m : ℕ} (i : Fin n) :
(castAdd m i).succ = if h : i.succ = last n then natAdd n 0 else castAdd (m + 1) ⟨↑i + 1, ⋯⟩
source
theorem Fin.succ_natAdd {n m : ℕ} (i : Fin m) :
(natAdd n i).succ = natAdd n i.succ

### pred #

source
theorem Fin.pred_one' {n : ℕ} [NeZero n] (h : 1 ≠ 0 := ⋯) :
pred 1 h = 0
source
theorem Fin.pred_last {n : ℕ} (h : ¬last (n + 1) = 0 := ⋯) :
(last (n + 1)).pred h = last n
source
theorem Fin.pred_lt_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) :
i.pred hi < j ↔ i < j.succ
source
theorem Fin.lt_pred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) :
j < i.pred hi ↔ j.succ < i
source
theorem Fin.pred_le_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) :
i.pred hi ≤ j ↔ i ≤ j.succ
source
theorem Fin.le_pred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) :
j ≤ i.pred hi ↔ j.succ ≤ i
source
theorem Fin.castSucc_pred_eq_pred_castSucc {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) :
(a.pred ha).castSucc = a.castSucc.pred ⋯
source
theorem Fin.castSucc_pred_add_one_eq {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) :
(a.pred ha).castSucc + 1 = a
source
theorem Fin.le_pred_castSucc_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.castSucc ≠ 0) :
b ≤ a.castSucc.pred ha ↔ b < a
source
theorem Fin.pred_castSucc_lt_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.castSucc ≠ 0) :
a.castSucc.pred ha < b ↔ a ≤ b
source
theorem Fin.pred_castSucc_lt {n : ℕ} {a : Fin (n + 1)} (ha : a.castSucc ≠ 0) :
a.castSucc.pred ha < a
source
theorem Fin.le_castSucc_pred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0) :
b ≤ (a.pred ha).castSucc ↔ b < a
source
theorem Fin.castSucc_pred_lt_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0) :
(a.pred ha).castSucc < b ↔ a ≤ b
source
theorem Fin.castSucc_pred_lt {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) :
(a.pred ha).castSucc < a
source
@[inline]
def Fin.castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ last n) :
Fin n

`castPred i` sends `i : Fin (n + 1)` to `Fin n` as long as i ≠ last n.

Equations

- i.castPred h = i.castLT ⋯

Instances For

source
@[simp]
theorem Fin.castLT_eq_castPred {n : ℕ} (i : Fin (n + 1)) (h : i < last n) (h' : ¬i = last n := ⋯) :
i.castLT h = i.castPred h'
source
@[simp]
theorem Fin.coe_castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ last n) :
↑(i.castPred h) = ↑i
source
@[simp]
theorem Fin.castPred_castSucc {n : ℕ} {i : Fin n} (h' : ¬i.castSucc = last n := ⋯) :
i.castSucc.castPred h' = i
source
@[simp]
theorem Fin.castSucc_castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ last n) :
(i.castPred h).castSucc = i
source
theorem Fin.castPred_eq_iff_eq_castSucc {n : ℕ} (i : Fin (n + 1)) (hi : i ≠ last n) (j : Fin n) :
i.castPred hi = j ↔ i = j.castSucc
source
@[simp]
theorem Fin.castPred_mk {n : ℕ} (i : ℕ) (h₁ : i < n) (h₂ : i < n.succ := ⋯) (h₃ : ⟨i, h₂⟩ ≠ last n := ⋯) :
⟨i, h₂⟩.castPred h₃ = ⟨i, h₁⟩
source
@[simp]
theorem Fin.castPred_le_castPred_iff {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ last n} {hj : j ≠ last n} :
i.castPred hi ≤ j.castPred hj ↔ i ≤ j
source
theorem Fin.castPred_le_castPred {n : ℕ} {i j : Fin (n + 1)} (h : i ≤ j) (hj : j ≠ last n) :
i.castPred ⋯ ≤ j.castPred hj

A version of the right-to-left implication of `castPred_le_castPred_iff` that deduces `i ≠ last n` from `i ≤ j` and `j ≠ last n`.

source
@[simp]
theorem Fin.castPred_lt_castPred_iff {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ last n} {hj : j ≠ last n} :
i.castPred hi < j.castPred hj ↔ i < j
source
theorem Fin.castPred_lt_castPred {n : ℕ} {i j : Fin (n + 1)} (h : i < j) (hj : j ≠ last n) :
i.castPred ⋯ < j.castPred hj

A version of the right-to-left implication of `castPred_lt_castPred_iff` that deduces `i ≠ last n` from `i < j`.

source
theorem Fin.castPred_lt_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) :
i.castPred hi < j ↔ i < j.castSucc
source
theorem Fin.lt_castPred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) :
j < i.castPred hi ↔ j.castSucc < i
source
theorem Fin.castPred_le_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) :
i.castPred hi ≤ j ↔ i ≤ j.castSucc
source
theorem Fin.le_castPred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) :
j ≤ i.castPred hi ↔ j.castSucc ≤ i
source
@[simp]
theorem Fin.castPred_inj {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ last n} {hj : j ≠ last n} :
i.castPred hi = j.castPred hj ↔ i = j
source
@[simp]
theorem Fin.castPred_zero {n : ℕ} [NeZero n] :
castPred 0 ⋯ = 0
source
@[deprecated Fin.castPred_zero (since := "2025-05-11")]
theorem Fin.castPred_zero' {n : ℕ} [NeZero n] :
castPred 0 ⋯ = 0

Alias of `Fin.castPred_zero`.

source
@[simp]
theorem Fin.castPred_eq_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} (h : i ≠ last n) :
i.castPred h = 0 ↔ i = 0
source
theorem Fin.castPred_ne_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} (h₁ : i ≠ last n) (h₂ : i ≠ 0) :
i.castPred h₁ ≠ 0
source
@[simp]
theorem Fin.castPred_one {n : ℕ} [NeZero n] :
castPred 1 ⋯ = 1
source
theorem Fin.succ_castPred_eq_castPred_succ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ last n) (ha' : a.succ ≠ last (n + 1) := ⋯) :
(a.castPred ha).succ = a.succ.castPred ha'
source
theorem Fin.succ_castPred_eq_add_one {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ last n) :
(a.castPred ha).succ = a + 1
source
theorem Fin.castpred_succ_le_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.succ ≠ last (n + 1)) :
a.succ.castPred ha ≤ b ↔ a < b
source
theorem Fin.lt_castPred_succ_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.succ ≠ last (n + 1)) :
b < a.succ.castPred ha ↔ b ≤ a
source
theorem Fin.lt_castPred_succ {n : ℕ} {a : Fin (n + 1)} (ha : a.succ ≠ last (n + 1)) :
a < a.succ.castPred ha
source
theorem Fin.succ_castPred_le_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ last n) :
(a.castPred ha).succ ≤ b ↔ a < b
source
theorem Fin.lt_succ_castPred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ last n) :
b < (a.castPred ha).succ ↔ b ≤ a
source
theorem Fin.lt_succ_castPred {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ last n) :
a < (a.castPred ha).succ
source
theorem Fin.castPred_le_pred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ last n) (hb : b ≠ 0) :
a.castPred ha ≤ b.pred hb ↔ a < b
source
theorem Fin.pred_lt_castPred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ last n) :
a.pred ha < b.castPred hb ↔ a ≤ b
source
theorem Fin.pred_lt_castPred {n : ℕ} {a : Fin (n + 1)} (h₁ : a ≠ 0) (h₂ : a ≠ last n) :
a.pred h₁ < a.castPred h₂
source
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

Instances For

source
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`.

source
theorem Fin.succAbove_of_succ_le {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : i.succ ≤ p) :
p.succAbove i = i.castSucc
source
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`.

source
theorem Fin.succAbove_of_lt_succ {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p < i.succ) :
p.succAbove i = i.succ
source
theorem Fin.succAbove_succ_of_lt {n : ℕ} (p i : Fin n) (h : p < i) :
p.succ.succAbove i = i.succ
source
theorem Fin.succAbove_succ_of_le {n : ℕ} (p i : Fin n) (h : i ≤ p) :
p.succ.succAbove i = i.castSucc
source
@[simp]
theorem Fin.succAbove_succ_self {n : ℕ} (j : Fin n) :
j.succ.succAbove j = j.castSucc
source
theorem Fin.succAbove_castSucc_of_lt {n : ℕ} (p i : Fin n) (h : i < p) :
p.castSucc.succAbove i = i.castSucc
source
theorem Fin.succAbove_castSucc_of_le {n : ℕ} (p i : Fin n) (h : p ≤ i) :
p.castSucc.succAbove i = i.succ
source
@[simp]
theorem Fin.succAbove_castSucc_self {n : ℕ} (j : Fin n) :
j.castSucc.succAbove j = j.succ
source
theorem Fin.succAbove_pred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : p < i) :
p.succAbove (i.pred ⋯) = i
source
theorem Fin.succAbove_pred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : i ≤ p) (hi : i ≠ 0) :
p.succAbove (i.pred hi) = (i.pred hi).castSucc
source
@[simp]
theorem Fin.succAbove_pred_self {n : ℕ} (p : Fin (n + 1)) (h : p ≠ 0) :
p.succAbove (p.pred h) = (p.pred h).castSucc
source
theorem Fin.succAbove_castPred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : i < p) :
p.succAbove (i.castPred ⋯) = i
source
theorem Fin.succAbove_castPred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : p ≤ i) (hi : i ≠ last n) :
p.succAbove (i.castPred hi) = (i.castPred hi).succ
source
theorem Fin.succAbove_castPred_self {n : ℕ} (p : Fin (n + 1)) (h : p ≠ last n) :
p.succAbove (p.castPred h) = (p.castPred h).succ
source
@[simp]
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

source
@[simp]
theorem Fin.ne_succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :
p ≠ p.succAbove i
source
theorem Fin.succAbove_right_injective {n : ℕ} {p : Fin (n + 1)} :
Function.Injective p.succAbove

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

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

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

source
@[simp]
theorem Fin.succAbove_ne_zero_zero {n : ℕ} [NeZero n] {a : Fin (n + 1)} (ha : a ≠ 0) :
a.succAbove 0 = 0
source
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
source
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
source
@[simp]
theorem Fin.succAbove_zero {n : ℕ} :
succAbove 0 = succ

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

source
theorem Fin.succAbove_zero_apply {n : ℕ} (i : Fin n) :
succAbove 0 i = i.succ
source
@[simp]
theorem Fin.succAbove_ne_last_last {n : ℕ} {a : Fin (n + 2)} (h : a ≠ last (n + 1)) :
a.succAbove (last n) = last (n + 1)
source
theorem Fin.succAbove_eq_last_iff {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last (n + 1)) :
a.succAbove b = last (n + 1) ↔ b = last n
source
theorem Fin.succAbove_ne_last {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last (n + 1)) (hb : b ≠ last n) :
a.succAbove b ≠ last (n + 1)
source
@[simp]
theorem Fin.succAbove_last {n : ℕ} :
(last n).succAbove = castSucc

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

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

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

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

source
theorem Fin.castPred_succAbove {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : x.castSucc < y) (h' : y.succAbove x ≠ last n := ⋯) :
(y.succAbove x).castPred h' = x
source
theorem Fin.pred_succAbove {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : y ≤ x.castSucc) (h' : y.succAbove x ≠ 0 := ⋯) :
(y.succAbove x).pred h' = x
source
theorem Fin.exists_succAbove_eq {n : ℕ} {x y : Fin (n + 1)} (h : x ≠ y) :
∃ (z : Fin n), y.succAbove z = x
source
@[simp]
theorem Fin.exists_succAbove_eq_iff {n : ℕ} {x y : Fin (n + 1)} :
(∃ (z : Fin n), x.succAbove z = y) ↔ y ≠ x
source
@[simp]
theorem Fin.range_succAbove {n : ℕ} (p : Fin (n + 1)) :
Set.range p.succAbove = {p}ᶜ

The range of `p.succAbove` is everything except `p`.

source
@[simp]
theorem Fin.range_succ (n : ℕ) :
Set.range succ = {0}ᶜ
source
theorem Fin.succAbove_left_injective {n : ℕ} :
Function.Injective succAbove

`succAbove` is injective at the pivot

source
@[simp]
theorem Fin.succAbove_left_inj {n : ℕ} {x y : Fin (n + 1)} :
x.succAbove = y.succAbove ↔ x = y

`succAbove` is injective at the pivot

source
@[simp]
theorem Fin.zero_succAbove {n : ℕ} (i : Fin n) :
succAbove 0 i = i.succ
source
theorem Fin.succ_succAbove_zero {n : ℕ} [NeZero n] (i : Fin n) :
i.succ.succAbove 0 = 0
source
@[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`.

source
@[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`.

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

`pred` commutes with `succAbove`.

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

`castPred` commutes with `succAbove`.

source
theorem Fin.one_succAbove_zero {n : ℕ} :
succAbove 1 0 = 0
source
@[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`.

source
@[simp]
theorem Fin.one_succAbove_succ {n : ℕ} (j : Fin n) :
succAbove 1 j.succ = j.succ.succ
source
@[simp]
theorem Fin.one_succAbove_one {n : ℕ} :
succAbove 1 1 = 2
source
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 ⋯

Instances For

source
theorem Fin.predAbove_of_le_castSucc {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i ≤ p.castSucc) :
p.predAbove i = i.castPred ⋯
source
theorem Fin.predAbove_of_lt_succ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i < p.succ) :
p.predAbove i = i.castPred ⋯
source
theorem Fin.predAbove_of_castSucc_lt {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.castSucc < i) :
p.predAbove i = i.pred ⋯
source
theorem Fin.predAbove_of_succ_le {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.succ ≤ i) :
p.predAbove i = i.pred ⋯
source
theorem Fin.predAbove_succ_of_lt {n : ℕ} (p i : Fin n) (h : i < p) :
p.predAbove i.succ = i.succ.castPred ⋯
source
theorem Fin.predAbove_succ_of_le {n : ℕ} (p i : Fin n) (h : p ≤ i) :
p.predAbove i.succ = i
source
@[simp]
theorem Fin.predAbove_succ_self {n : ℕ} (p : Fin n) :
p.predAbove p.succ = p
source
theorem Fin.predAbove_castSucc_of_lt {n : ℕ} (p i : Fin n) (h : p < i) :
p.predAbove i.castSucc = i.castSucc.pred ⋯
source
theorem Fin.predAbove_castSucc_of_le {n : ℕ} (p i : Fin n) (h : i ≤ p) :
p.predAbove i.castSucc = i
source
@[simp]
theorem Fin.predAbove_castSucc_self {n : ℕ} (p : Fin n) :
p.predAbove p.castSucc = p
source
theorem Fin.predAbove_pred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : i < p) :
(p.pred ⋯).predAbove i = i.castPred ⋯
source
theorem Fin.predAbove_pred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : p ≤ i) (hp : p ≠ 0) :
(p.pred hp).predAbove i = i.pred ⋯
source
theorem Fin.predAbove_pred_self {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ 0) :
(p.pred hp).predAbove p = p.pred hp
source
theorem Fin.predAbove_castPred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : p < i) :
(p.castPred ⋯).predAbove i = i.pred ⋯
source
theorem Fin.predAbove_castPred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : i ≤ p) (hp : p ≠ last n) :
(p.castPred hp).predAbove i = i.castPred ⋯
source
theorem Fin.predAbove_castPred_self {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ last n) :
(p.castPred hp).predAbove p = p.castPred hp
source
@[simp]
theorem Fin.predAbove_right_zero {n : ℕ} [NeZero n] {i : Fin n} :
i.predAbove 0 = 0
source
theorem Fin.predAbove_zero_succ {n : ℕ} [NeZero n] {i : Fin n} :
predAbove 0 i.succ = i
source
@[simp]
theorem Fin.predAbove_zero_of_ne_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} (hi : i ≠ 0) :
predAbove 0 i = i.pred hi
source
theorem Fin.succ_predAbove_zero {n : ℕ} [NeZero n] {j : Fin (n + 1)} (h : j ≠ 0) :
(predAbove 0 j).succ = j
source
theorem Fin.predAbove_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} :
predAbove 0 i = if hi : i = 0 then 0 else i.pred hi
source
@[simp]
theorem Fin.predAbove_right_last {n : ℕ} {i : Fin (n + 1)} :
i.predAbove (last (n + 1)) = last n
source
theorem Fin.predAbove_last_castSucc {n : ℕ} {i : Fin (n + 1)} :
(last n).predAbove i.castSucc = i
source
@[simp]
theorem Fin.predAbove_last_of_ne_last {n : ℕ} {i : Fin (n + 2)} (hi : i ≠ last (n + 1)) :
(last n).predAbove i = i.castPred hi
source
theorem Fin.predAbove_last_apply {n : ℕ} {i : Fin (n + 2)} :
(last n).predAbove i = if hi : i = last (n + 1) then last n else i.castPred hi
source
theorem Fin.predAbove_surjective {n : ℕ} (p : Fin n) :
Function.Surjective p.predAbove
source
@[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`.

source
@[simp]
theorem Fin.succ_succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.succ) :
p.succ.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.succ` is the identity away from `p.succ`.

source
@[simp]
theorem Fin.predAbove_succAbove {n : ℕ} (p 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.

source
@[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`.

source
@[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`.

source
theorem Fin.predAbove_predAbove_succAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
(j.predAbove i).predAbove (i.succAbove j) = j
source
theorem Fin.succAbove_succAbove_predAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
(i.succAbove j).succAbove (j.predAbove i) = i
source
theorem Fin.succAbove_succAbove_succAbove_predAbove {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (k : Fin n) :
(i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k)

Given `i : Fin (n + 2)` and `j : Fin (n + 1)`, there are two ways to represent the order embedding `Fin n → Fin (n + 2)` leaving holes at `i` and `i.succAbove j`.

One is `i.succAbove ∘ j.succAbove`. It corresponds to embedding `Fin n` to `Fin (n + 1)` leaving a hole at `j`, then embedding the result to `Fin (n + 2)` leaving a hole at `i`. The other one is `(i.succAbove j).succAbove ∘ (j.predAbove i).succAbove`. It corresponds to swapping the roles of `i` and `j`.

This lemma says that these two ways are equal. It is used in `Fin.removeNth_removeNth_eq_swap` to show that two ways of removing 2 elements from a sequence give the same answer.