The finite type with `n` elements #

Fin n is the type whose elements are natural numbers smaller than n. This file expands on the development in the core library.

Main definitions #

Induction principles #

finZeroElim : Elimination principle for the empty set Fin 0, generalizes Fin.elim0.
Fin.succRec : Define C n i by induction on i : Fin n interpreted as (0 : Fin (n - i)).succ.succ…. This function has two arguments: H0 n defines 0-th element C (n+1) 0 of an (n+1)-tuple, and Hs n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.
Fin.succRecOn : same as Fin.succRec but i : Fin n is the first argument;
Fin.induction : Define C i by induction on i : Fin (n + 1), separating into the Nat-like base cases of C 0 and C (i.succ).
Fin.inductionOn : same as Fin.induction but with i : Fin (n + 1) as the first argument.
Fin.cases : define f : Π i : Fin n.succ, C i by separately handling the cases i = 0 and i = Fin.succ j, j : Fin n, defined using Fin.induction.
Fin.reverseInduction: reverse induction on i : Fin (n + 1); given C (Fin.last n) and ∀ i : Fin n, C (Fin.succ i) → C (Fin.castSucc i), constructs all values C i by going down;
Fin.lastCases: define f : Π i, Fin (n + 1), C i by separately handling the cases i = Fin.last n and i = Fin.castSucc j, a special case of Fin.reverseInduction;
Fin.addCases: define a function on Fin (m + n) by separately handling the cases Fin.castAdd n i and Fin.natAdd m i;
Fin.succAbove_cases: given i : Fin (n + 1), define a function on Fin (n + 1) by separately handling the cases j = i and j = Fin.succAbove i k, same as Fin.insertNth but marked as eliminator and works for Sort*. -- Porting note: this is in another file

Order embeddings and an order isomorphism #

Fin.orderIsoSubtype : coercion to { i // i < n } as an OrderIso;
Fin.valEmbedding : coercion to natural numbers as an Embedding;
Fin.valOrderEmbedding : coercion to natural numbers as an OrderEmbedding;
Fin.succEmbedding : Fin.succ as an OrderEmbedding;
Fin.castLe h : embed Fin n into Fin m, h : n ≤ m;
Fin.cast : order isomorphism between Fin n and Fin m provided that n = m, see also Equiv.finCongr;
Fin.castAdd m : embed Fin n into Fin (n+m);
Fin.castSucc : embed Fin n into Fin (n+1);
Fin.succAbove p : embed Fin n into Fin (n + 1) with a hole around p;
Fin.addNat m i : add m on i on the right, generalizes Fin.succ;
Fin.natAdd n i adds n on i on the left;

Other casts #

Fin.ofNat': given a positive number n (deduced from [NeZero n]), Fin.ofNat' i is i % n interpreted as an element of Fin n;
Fin.castLt i h : embed i into a Fin where h proves it belongs into;
Fin.predAbove (p : Fin n) i : embed i : Fin (n+1) into Fin n by subtracting one if p < i;
Fin.castPred : embed Fin (n + 2) into Fin (n + 1) by mapping Fin.last (n + 1) to Fin.last n;
Fin.subNat i h : subtract m from i ≥ m, generalizes Fin.pred;
Fin.clamp n m : min n m as an element of Fin (m + 1);
Fin.divNat i : divides i : Fin (m * n) by n;
Fin.modNat i : takes the mod of i : Fin (m * n) by n;

Misc definitions #

Fin.last n : The greatest value of Fin (n+1).
Fin.rev : Fin n → Fin n : the antitone involution given by i ↦ n-(i+1)

source

ink

def finZeroElim {α : Fin 0 → Sort u_1} (x : Fin 0) :

α x

Elimination principle for the empty set Fin 0, dependent version.

Equations

finZeroElim x = Fin.elim0 x

source

ink

def Fin.elim0' {α : Sort u_1} (x : Fin 0) :

A non-dependent variant of elim0.

Equations

Fin.elim0' x = Fin.elim0 x

source

ink

theorem Fin.val_injective {n : ℕ} :

Function.Injective Fin.val

source

ink

theorem Fin.size_positive {n : ℕ} :

Fin n → 0 < n

If you actually have an element of Fin n, then the n is always positive

source

ink

theorem Fin.mod_def {n : ℕ} (a : Fin n) (m : Fin n) :

a % m = { val := ↑a % ↑m % n, isLt := (_ : ↑a % ↑m % n < n) }

source

ink

theorem Fin.add_def {n : ℕ} (a : Fin n) (b : Fin n) :

a + b = { val := (↑a + ↑b) % n, isLt := (_ : (↑a + ↑b) % n < n) }

source

ink

theorem Fin.mul_def {n : ℕ} (a : Fin n) (b : Fin n) :

a * b = { val := ↑a * ↑b % n, isLt := (_ : ↑a * ↑b % n < n) }

source

ink

theorem Fin.sub_def {n : ℕ} (a : Fin n) (b : Fin n) :

a - b = { val := (↑a + (n - ↑b)) % n, isLt := (_ : (↑a + (n - ↑b)) % n < n) }

source

ink

theorem Fin.size_positive' {n : ℕ} [inst : Nonempty (Fin n)] :

0 < n

source

ink

theorem Fin.prop {n : ℕ} (a : Fin n) :

↑a < n

source

ink

@[simp]

theorem Fin.is_lt {n : ℕ} (a : Fin n) :

↑a < n

source

ink

theorem Fin.pos {n : ℕ} (i : Fin n) :

0 < n

source

ink

theorem Fin.pos_iff_nonempty {n : ℕ} :

0 < n ↔ Nonempty (Fin n)

source

ink

@[simp]

theorem Fin.equivSubtype_symm_apply {n : ℕ} (a : { i // i < n }) :

↑(Equiv.symm Fin.equivSubtype) a = { val := ↑a, isLt := (_ : ↑a < n) }

source

ink

@[simp]

theorem Fin.equivSubtype_apply {n : ℕ} (a : Fin n) :

↑Fin.equivSubtype a = { val := ↑a, property := (_ : ↑a < n) }

source

ink

def Fin.equivSubtype {n : ℕ} :

Fin n ≃ { i // i < n }

Equivalence between Fin n and { i // i < n }.

Equations

One or more equations did not get rendered due to their size.

coercions and constructions #

source

ink

@[simp]

theorem Fin.eta {n : ℕ} (a : Fin n) (h : ↑a < n) :

{ val := ↑a, isLt := h } = a

source

ink

theorem Fin.ext {n : ℕ} {a : Fin n} {b : Fin n} (h : ↑a = ↑b) :

a = b

source

ink

theorem Fin.ext_iff {n : ℕ} {a : Fin n} {b : Fin n} :

a = b ↔ ↑a = ↑b

source

ink

theorem Fin.val_eq_val {n : ℕ} (a : Fin n) (b : Fin n) :

↑a = ↑b ↔ a = b

source

ink

theorem Fin.eq_iff_veq {n : ℕ} (a : Fin n) (b : Fin n) :

a = b ↔ ↑a = ↑b

source

ink

theorem Fin.ne_iff_vne {n : ℕ} (a : Fin n) (b : Fin n) :

a ≠ b ↔ ↑a ≠ ↑b

source

ink

@[simp]

theorem Fin.mk_eq_mk {n : ℕ} {a : ℕ} {h : a < n} {a' : ℕ} {h' : a' < n} :

{ val := a, isLt := h } = { val := a', isLt := h' } ↔ a = a'

source

ink

theorem Fin.mk.inj_iff {n : ℕ} {a : ℕ} {b : ℕ} {ha : a < n} {hb : b < n} :

{ val := a, isLt := ha } = { val := b, isLt := hb } ↔ a = b

source

ink

theorem Fin.val_mk {m : ℕ} {n : ℕ} (h : m < n) :

↑{ val := m, isLt := h } = m

source

ink

theorem Fin.eq_mk_iff_val_eq {n : ℕ} {a : Fin n} {k : ℕ} {hk : k < n} :

a = { val := k, isLt := hk } ↔ ↑a = k

source

ink

theorem Fin.mk_val {n : ℕ} (i : Fin n) :

{ val := ↑i, isLt := (_ : ↑i < n) } = i

source

ink

theorem Fin.heq_fun_iff {α : Sort u_1} {k : ℕ} {l : ℕ} (h : k = l) {f : Fin k → α} {g : Fin l → α} :

HEq f g ↔ ∀ (i : Fin k), f i = g { val := ↑i, isLt := (_ : ↑i < l) }

Assume k = l. If two functions defined on Fin k and Fin l are equal on each element, then they coincide (in the heq sense).

source

ink

theorem Fin.heq_ext_iff {k : ℕ} {l : ℕ} (h : k = l) {i : Fin k} {j : Fin l} :

HEq i j ↔ ↑i = ↑j

source

ink

theorem Fin.exists_iff {n : ℕ} {p : Fin n → Prop} :

(∃ i, p i) ↔ ∃ i h, p { val := i, isLt := h }

source

ink

theorem Fin.forall_iff {n : ℕ} {p : Fin n → Prop} :

((i : Fin n) → p i) ↔ (i : ℕ) → (h : i < n) → p { val := i, isLt := h }

order #

source

ink

theorem Fin.is_le {n : ℕ} (i : Fin (n + 1)) :

↑i ≤ n

source

ink

@[simp]

theorem Fin.is_le' {n : ℕ} {a : Fin n} :

↑a ≤ n

source

ink

theorem Fin.lt_iff_val_lt_val {n : ℕ} {a : Fin n} {b : Fin n} :

a < b ↔ ↑a < ↑b

source

ink

theorem Fin.le_iff_val_le_val {n : ℕ} {a : Fin n} {b : Fin n} :

a ≤ b ↔ ↑a ≤ ↑b

source

ink

theorem Fin.mk_lt_of_lt_val {n : ℕ} {b : Fin n} {a : ℕ} (h : a < ↑b) :

{ val := a, isLt := (_ : a < n) } < b

source

ink

theorem Fin.mk_le_of_le_val {n : ℕ} {b : Fin n} {a : ℕ} (h : a ≤ ↑b) :

{ val := a, isLt := (_ : a < n) } ≤ b

source

ink

@[simp]

theorem Fin.val_fin_lt {n : ℕ} {a : Fin n} {b : Fin n} :

↑a < ↑b ↔ a < b

a < b as natural numbers if and only if a < b in Fin n.

source

ink

@[simp]

theorem Fin.val_fin_le {n : ℕ} {a : Fin n} {b : Fin n} :

↑a ≤ ↑b ↔ a ≤ b

a ≤ b as natural numbers if and only if a ≤ b in Fin n.

source

ink

instance Fin.instLinearOrderFin {n : ℕ} :

LinearOrder (Fin n)

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Fin.mk_le_mk {n : ℕ} {x : ℕ} {y : ℕ} {hx : x < n} {hy : y < n} :

{ val := x, isLt := hx } ≤ { val := y, isLt := hy } ↔ x ≤ y

source

ink

@[simp]

theorem Fin.mk_lt_mk {n : ℕ} {x : ℕ} {y : ℕ} {hx : x < n} {hy : y < n} :

{ val := x, isLt := hx } < { val := y, isLt := hy } ↔ x < y

source

ink

theorem Fin.min_val {n : ℕ} {a : Fin n} :

min (↑a) n = ↑a

source

ink

theorem Fin.max_val {n : ℕ} {a : Fin n} :

max (↑a) n = n

source

ink

instance Fin.instPartialOrderFin {n : ℕ} :

PartialOrder (Fin n)

Equations

Fin.instPartialOrderFin = inferInstance

source

ink

theorem Fin.val_strictMono {n : ℕ} :

StrictMono Fin.val

source

ink

@[simp]

theorem Fin.orderIsoSubtype_apply {n : ℕ} (a : Fin n) :

↑(RelIso.toRelEmbedding Fin.orderIsoSubtype).toEmbedding a = { val := ↑a, property := (_ : ↑a < n) }

source

ink

@[simp]

theorem Fin.orderIsoSubtype_symm_apply {n : ℕ} (a : { i // i < n }) :

↑(RelIso.toRelEmbedding (RelIso.symm Fin.orderIsoSubtype)).toEmbedding a = { val := ↑a, isLt := (_ : ↑a < n) }

source

ink

def Fin.orderIsoSubtype {n : ℕ} :

Fin n ≃o { i // i < n }

The equivalence Fin n ≃ { i // i < n } is an order isomorphism.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Fin.valEmbedding_apply {n : ℕ} (self : Fin n) :

↑Fin.valEmbedding self = ↑self

source

ink

def Fin.valEmbedding {n : ℕ} :

Fin n ↪ ℕ

The inclusion map Fin n → ℕ is an embedding.

Equations

Fin.valEmbedding = { toFun := Fin.val, inj' := (_ : Function.Injective Fin.val) }

source

ink

@[simp]

theorem Fin.equivSubtype_symm_trans_valEmbedding {n : ℕ} :

Function.Embedding.trans (Equiv.toEmbedding (Equiv.symm Fin.equivSubtype)) Fin.valEmbedding = Function.Embedding.subtype fun x => x < n

source

ink

@[simp]

theorem Fin.valOrderEmbedding_apply (n : ℕ) (self : Fin n) :

↑(Fin.valOrderEmbedding n).toEmbedding self = ↑self

source

ink

def Fin.valOrderEmbedding (n : ℕ) :

Fin n ↪o ℕ

The inclusion map Fin n → ℕ is an order embedding.

Equations

Fin.valOrderEmbedding n = { toEmbedding := Fin.valEmbedding, map_rel_iff' := (_ : ∀ {a b : Fin n}, ↑Fin.valEmbedding a ≤ ↑Fin.valEmbedding b ↔ ↑Fin.valEmbedding a ≤ ↑Fin.valEmbedding b) }

source

ink

instance Fin.Lt.isWellOrder (n : ℕ) :

IsWellOrder (Fin n) fun x x_1 => x < x_1

The ordering on Fin n is a well order.

Equations

Fin.Lt.isWellOrder = Fin.Lt.isWellOrder.proof_1

source

ink

instance Fin.instWellFoundedRelationFin {n : ℕ} :

WellFoundedRelation (Fin n)

Use the ordering on Fin n for checking recursive definitions.

For example, the following definition is not accepted by the termination checker, unless we declare the WellFoundedRelation instance:

def factorial {n : ℕ} : Fin n → ℕ
| ⟨0, _⟩ := 1
| ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩

Equations

Fin.instWellFoundedRelationFin = measure Fin.val

source

ink

def Fin.ofNat'' {n : ℕ} [inst : NeZero n] (i : ℕ) :

Fin n

Given a positive n, Fin.ofNat' i is i % n as an element of Fin n.

Equations

Fin.ofNat'' i = { val := i % n, isLt := (_ : i % n < n) }

source

ink

instance Fin.instZeroFin {n : ℕ} [inst : NeZero n] :

Zero (Fin n)

Equations

Fin.instZeroFin = { zero := Fin.ofNat'' 0 }

source

ink

instance Fin.instOneFin {n : ℕ} [inst : NeZero n] :

One (Fin n)

Equations

Fin.instOneFin = { one := Fin.ofNat'' 1 }

source

ink

@[simp]

theorem Fin.val_zero (n : ℕ) [inst : NeZero n] :

↑0 = 0

source

ink

@[simp]

theorem Fin.mk_zero {n : ℕ} [inst : NeZero n] :

{ val := 0, isLt := (_ : 0 < n) } = 0

source

ink

@[simp]

theorem Fin.zero_le {n : ℕ} [inst : NeZero n] (a : Fin n) :

0 ≤ a

source

ink

theorem Fin.zero_lt_one {n : ℕ} :

0 < 1

source

ink

@[simp]

theorem Fin.not_lt_zero {n : ℕ} (a : Fin (Nat.succ n)) :

¬a < 0

source

ink

theorem Fin.pos_iff_ne_zero {n : ℕ} [inst : NeZero n] (a : Fin n) :

0 < a ↔ a ≠ 0

source

ink

theorem Fin.eq_zero_or_eq_succ {n : ℕ} (i : Fin (n + 1)) :

i = 0 ∨ ∃ j, i = Fin.succ j

source

ink

theorem Fin.eq_succ_of_ne_zero {n : ℕ} {i : Fin (n + 1)} (hi : i ≠ 0) :

∃ j, i = Fin.succ j

source

ink

def Fin.rev {n : ℕ} :

Equiv.Perm (Fin n)

The antitone involution Fin n → Fin n given by i ↦ n-(i+1).

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Fin.val_rev {n : ℕ} (i : Fin n) :

↑(↑Fin.rev i) = n - (↑i + 1)

source

ink

theorem Fin.rev_involutive {n : ℕ} :

Function.Involutive ↑Fin.rev

source

ink

theorem Fin.rev_injective {n : ℕ} :

Function.Injective ↑Fin.rev

source

ink

theorem Fin.rev_surjective {n : ℕ} :

Function.Surjective ↑Fin.rev

source

ink

theorem Fin.rev_bijective {n : ℕ} :

Function.Bijective ↑Fin.rev

source

ink

theorem Fin.rev_inj {n : ℕ} {i : Fin n} {j : Fin n} :

↑Fin.rev i = ↑Fin.rev j ↔ i = j

source

ink

@[simp]

theorem Fin.rev_rev {n : ℕ} (i : Fin n) :

↑Fin.rev (↑Fin.rev i) = i

source

ink

@[simp]

theorem Fin.rev_symm {n : ℕ} :

Equiv.symm Fin.rev = Fin.rev

source

ink

theorem Fin.rev_eq {n : ℕ} {a : ℕ} (i : Fin (n + 1)) (h : n = a + ↑i) :

↑Fin.rev i = { val := a, isLt := (_ : a < Nat.succ n) }

source

ink

@[simp]

theorem Fin.rev_le_rev {n : ℕ} {i : Fin n} {j : Fin n} :

↑Fin.rev i ≤ ↑Fin.rev j ↔ j ≤ i

source

ink

@[simp]

theorem Fin.rev_lt_rev {n : ℕ} {i : Fin n} {j : Fin n} :

↑Fin.rev i < ↑Fin.rev j ↔ j < i

source

ink

@[simp]

theorem Fin.revOrderIso_apply {n : ℕ} :

∀ (a : (Fin n)ᵒᵈ), ↑(RelIso.toRelEmbedding Fin.revOrderIso).toEmbedding a = ↑Fin.rev (↑OrderDual.ofDual a)

source

ink

@[simp]

theorem Fin.revOrderIso_toEquiv {n : ℕ} :

Fin.revOrderIso.toEquiv = Equiv.trans OrderDual.ofDual Fin.rev

source

ink

def Fin.revOrderIso {n : ℕ} :

(Fin n)ᵒᵈ ≃o Fin n

Fin.rev n as an order-reversing isomorphism.

Equations

Fin.revOrderIso = { toEquiv := Equiv.trans OrderDual.ofDual Fin.rev, map_rel_iff' := (_ : ∀ {a b : (Fin n)ᵒᵈ}, ↑Fin.rev a ≤ ↑Fin.rev b ↔ b ≤ a) }

source

ink

@[simp]

theorem Fin.revOrderIso_symm_apply {n : ℕ} (i : Fin n) :

↑(RelIso.toRelEmbedding (OrderIso.symm Fin.revOrderIso)).toEmbedding i = ↑OrderDual.toDual (↑Fin.rev i)

source

ink

def Fin.last (n : ℕ) :

Fin (n + 1)

The greatest value of Fin (n+1)

Equations

Fin.last n = { val := n, isLt := (_ : n < Nat.succ n) }

source

ink

@[simp]

theorem Fin.val_last (n : ℕ) :

↑(Fin.last n) = n

source

ink

theorem Fin.le_last {n : ℕ} (i : Fin (n + 1)) :

i ≤ Fin.last n

source

ink

instance Fin.instBoundedOrderFinHAddNatInstHAddInstAddNatOfNatInstLEFin {n : ℕ} :

BoundedOrder (Fin (n + 1))

Equations

Fin.instBoundedOrderFinHAddNatInstHAddInstAddNatOfNatInstLEFin = BoundedOrder.mk

source

ink

instance Fin.instLatticeFinHAddNatInstHAddInstAddNatOfNat {n : ℕ} :

Lattice (Fin (n + 1))

Equations

Fin.instLatticeFinHAddNatInstHAddInstAddNatOfNat = LinearOrder.toLattice

source

ink

theorem Fin.last_pos {n : ℕ} :

0 < Fin.last (n + 1)

source

ink

theorem Fin.eq_last_of_not_lt {n : ℕ} {i : Fin (n + 1)} (h : ¬↑i < n) :

i = Fin.last n

source

ink

theorem Fin.val_lt_last {n : ℕ} {i : Fin (n + 1)} (h : i ≠ Fin.last n) :

↑i < n

source

ink

theorem Fin.top_eq_last (n : ℕ) :

⊤ = Fin.last n

source

ink

theorem Fin.bot_eq_zero (n : ℕ) :

⊥ = 0

source

ink

@[simp]

theorem Fin.coe_orderIso_apply {n : ℕ} {m : ℕ} (e : Fin n ≃o Fin m) (i : Fin n) :

↑(↑(RelIso.toRelEmbedding e).toEmbedding i) = ↑i

If e is an orderIso between Fin n and Fin m, then n = m and e is the identity map. In this lemma we state that for each i : Fin n we have (e i : ℕ) = (i : ℕ).

source

ink

instance Fin.orderIso_subsingleton {n : ℕ} {α : Type u_1} [inst : Preorder α] :

Subsingleton (Fin n ≃o α)

Equations

@Fin.orderIso_subsingleton = @Fin.orderIso_subsingleton.proof_1

source

ink

instance Fin.orderIso_subsingleton' {n : ℕ} {α : Type u_1} [inst : Preorder α] :

Subsingleton (α ≃o Fin n)

Equations

@Fin.orderIso_subsingleton' = @Fin.orderIso_subsingleton'.proof_1

source

ink

instance Fin.orderIsoUnique {n : ℕ} :

Unique (Fin n ≃o Fin n)

Equations

Fin.orderIsoUnique = Unique.mk' (Fin n ≃o Fin n)

source

ink

theorem Fin.strictMono_unique {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin n → α} {g : Fin n → α} (hf : StrictMono f) (hg : StrictMono g) (h : Set.range f = Set.range g) :

f = g

Two strictly monotone functions from Fin n are equal provided that their ranges are equal.

source

ink

theorem Fin.orderEmbedding_eq {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin n ↪o α} {g : Fin n ↪o α} (h : Set.range ↑f.toEmbedding = Set.range ↑g.toEmbedding) :

f = g

Two order embeddings of Fin n are equal provided that their ranges are equal.

addition, numerals, and coercion from Nat #

source

ink

@[simp]

theorem Fin.val_one (n : ℕ) :

↑1 = 1

source

ink

@[simp]

theorem Fin.val_one' (n : ℕ) [inst : NeZero n] :

↑1 = 1 % n

source

ink

theorem Fin.val_one'' {n : ℕ} :

↑1 = 1 % (n + 1)

source

ink

@[simp]

theorem Fin.mk_one {n : ℕ} :

{ val := 1, isLt := (_ : Nat.succ 0 < Nat.succ (n + 1)) } = 1

source

ink

instance Fin.nontrivial {n : ℕ} :

Nontrivial (Fin (n + 2))

Equations

@Fin.nontrivial = @Fin.nontrivial.proof_1

source

ink

theorem Fin.nontrivial_iff_two_le {n : ℕ} :

Nontrivial (Fin n) ↔ 2 ≤ n

source

ink

theorem Fin.subsingleton_iff_le_one {n : ℕ} :

Subsingleton (Fin n) ↔ n ≤ 1

source

ink

theorem Fin.add_zero {n : ℕ} [inst : NeZero n] (k : Fin n) :

k + 0 = k

source

ink

theorem Fin.zero_add {n : ℕ} [inst : NeZero n] (k : Fin n) :

0 + k = k

source

ink

instance Fin.instOfNatFin {n : ℕ} {a : ℕ} [inst : NeZero n] :

OfNat (Fin n) a

Equations

Fin.instOfNatFin = { ofNat := Fin.ofNat' a (_ : 0 < n) }

source

ink

@[simp]

theorem Fin.ofNat'_zero {n : ℕ} {h : n > 0} [inst : NeZero n] :

Fin.ofNat' 0 h = 0

source

ink

@[simp]

theorem Fin.ofNat'_one {n : ℕ} {h : n > 0} [inst : NeZero n] :

Fin.ofNat' 1 h = 1

source

ink

instance Fin.instAddCommSemigroupFin (n : ℕ) :

AddCommSemigroup (Fin n)

Equations

Fin.instAddCommSemigroupFin n = AddCommSemigroup.mk (_ : ∀ (a a_1 : Fin n), a + a_1 = a_1 + a)

source

ink

instance Fin.addCommMonoid (n : ℕ) [inst : NeZero n] :

AddCommMonoid (Fin n)

Equations

Fin.addCommMonoid n = AddCommMonoid.mk (_ : ∀ (a a_1 : Fin n), a + a_1 = a_1 + a)

source

ink

instance Fin.instAddMonoidWithOneFin (n : ℕ) [inst : NeZero n] :

AddMonoidWithOne (Fin n)

Equations

Fin.instAddMonoidWithOneFin n = let src := inferInstanceAs (AddCommMonoid (Fin n)); AddMonoidWithOne.mk

source

ink

theorem Fin.val_add {n : ℕ} (a : Fin n) (b : Fin n) :

↑(a + b) = (↑a + ↑b) % n

source

ink

theorem Fin.val_add_eq_ite {n : ℕ} (a : Fin n) (b : Fin n) :

↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b

source

ink

theorem Fin.val_bit0 {n : ℕ} (k : Fin n) :

↑(bit0 k) = bit0 ↑k % n

source

ink

theorem Fin.val_bit1 {n : ℕ} [inst : NeZero n] (k : Fin n) :

↑(bit1 k) = bit1 ↑k % n

source

ink

theorem Fin.val_add_one_of_lt {n : ℕ} {i : Fin (Nat.succ n)} (h : i < Fin.last n) :

↑(i + 1) = ↑i + 1

source

ink

@[simp]

theorem Fin.last_add_one (n : ℕ) :

Fin.last n + 1 = 0

source

ink

theorem Fin.val_add_one {n : ℕ} (i : Fin (n + 1)) :

↑(i + 1) = if i = Fin.last n then 0 else ↑i + 1

source

ink

@[simp]

theorem Fin.mk_bit0 {m : ℕ} {n : ℕ} (h : bit0 m < n) :

{ val := bit0 m, isLt := h } = bit0 { val := m, isLt := (_ : m < n) }

source

ink

@[simp]

theorem Fin.mk_bit1 {m : ℕ} {n : ℕ} [inst : NeZero n] (h : bit1 m < n) :

{ val := bit1 m, isLt := h } = bit1 { val := m, isLt := (_ : m < n) }

source

ink

@[simp]

theorem Fin.val_two {n : ℕ} :

↑2 = 2

source

ink

@[simp]

theorem Fin.ofNat_eq_val (n : ℕ) [inst : NeZero n] (a : ℕ) :

Fin.ofNat'' a = ↑a

source

ink

theorem Fin.val_cast_of_lt {n : ℕ} [inst : NeZero n] {a : ℕ} (h : a < n) :

↑↑a = a

Converting an in-range number to Fin (n + 1) produces a result whose value is the original number.

source

ink

theorem Fin.cast_val_eq_self {n : ℕ} [inst : NeZero n] (a : Fin n) :

↑↑a = a

Converting the value of a Fin (n + 1) to Fin (n + 1) results in the same value.

source

ink

theorem Fin.cast_nat_eq_last (n : ℕ) :

↑n = Fin.last n

source

ink

theorem Fin.le_val_last {n : ℕ} (i : Fin (n + 1)) :

i ≤ ↑n

source

ink

theorem Fin.add_one_pos {n : ℕ} (i : Fin (n + 1)) (h : i < Fin.last n) :

0 < i + 1

source

ink

theorem Fin.one_pos {n : ℕ} :

0 < 1

source

ink

theorem Fin.zero_ne_one {n : ℕ} :

0 ≠ 1

source

ink

@[simp]

theorem Fin.zero_eq_one_iff {n : ℕ} [inst : NeZero n] :

0 = 1 ↔ n = 1

source

ink

@[simp]

theorem Fin.one_eq_zero_iff {n : ℕ} [inst : NeZero n] :

1 = 0 ↔ n = 1

succ and casts into larger Fin types #

source

ink

@[simp]

theorem Fin.val_succ {n : ℕ} (j : Fin n) :

↑(Fin.succ j) = ↑j + 1

source

ink

@[simp]

theorem Fin.succ_pos {n : ℕ} (a : Fin n) :

0 < Fin.succ a

source

ink

def Fin.succEmbedding (n : ℕ) :

Fin n ↪o Fin (n + 1)

Fin.succ as an OrderEmbedding

Equations

Fin.succEmbedding n = OrderEmbedding.ofStrictMono Fin.succ (_ : ∀ (x x_1 : Fin n), x < x_1 → Nat.succ ↑x < Nat.succ ↑x_1)

source

ink

@[simp]

theorem Fin.val_succEmbedding {n : ℕ} :

↑(Fin.succEmbedding n).toEmbedding = Fin.succ

source

ink

@[simp]

theorem Fin.succ_le_succ_iff {n : ℕ} {a : Fin n} {b : Fin n} :

Fin.succ a ≤ Fin.succ b ↔ a ≤ b

source

ink

@[simp]

theorem Fin.succ_lt_succ_iff {n : ℕ} {a : Fin n} {b : Fin n} :

Fin.succ a < Fin.succ b ↔ a < b

source

ink

theorem Fin.succ_injective (n : ℕ) :

Function.Injective Fin.succ

source

ink

@[simp]

theorem Fin.succ_inj {n : ℕ} {a : Fin n} {b : Fin n} :

Fin.succ a = Fin.succ b ↔ a = b

source

ink

theorem Fin.succ_ne_zero {n : ℕ} (k : Fin n) :

Fin.succ k ≠ 0

source

ink

@[simp]

theorem Fin.succ_zero_eq_one {n : ℕ} [inst : NeZero n] :

Fin.succ 0 = 1

source

ink

@[simp]

theorem Fin.succ_zero_eq_one' {n : ℕ} :

Fin.succ 0 = 1

Version of succ_zero_eq_one to be used by dsimp

source

ink

@[simp]

theorem Fin.succ_one_eq_two {n : ℕ} [inst : NeZero n] :

Fin.succ 1 = 2

source

ink

@[simp]

theorem Fin.succ_one_eq_two' {n : ℕ} :

Fin.succ 1 = 2

Version of succ_one_eq_two to be used by dsimp

source

ink

@[simp]

theorem Fin.succ_mk (n : ℕ) (i : ℕ) (h : i < n) :

Fin.succ { val := i, isLt := h } = { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }

source

ink

theorem Fin.mk_succ_pos {n : ℕ} (i : ℕ) (h : i < n) :

0 < { val := Nat.succ i, isLt := (_ : i + 1 < n + 1) }

source

ink

theorem Fin.one_lt_succ_succ {n : ℕ} (a : Fin n) :

1 < Fin.succ (Fin.succ a)

source

ink

@[simp]

theorem Fin.add_one_lt_iff {n : ℕ} {k : Fin (n + 2)} :

k + 1 < k ↔ k = Fin.last (n + 1)

source

ink

@[simp]

theorem Fin.add_one_le_iff {n : ℕ} {k : Fin (n + 1)} :

k + 1 ≤ k ↔ k = Fin.last n

source

ink

@[simp]

theorem Fin.last_le_iff {n : ℕ} {k : Fin (n + 1)} :

Fin.last n ≤ k ↔ k = Fin.last n

source

ink

@[simp]

theorem Fin.lt_add_one_iff {n : ℕ} {k : Fin (n + 1)} :

k < k + 1 ↔ k < Fin.last n

source

ink

@[simp]

theorem Fin.le_zero_iff {n : ℕ} [inst : NeZero n] {k : Fin n} :

k ≤ 0 ↔ k = 0

source

ink

theorem Fin.succ_succ_ne_one {n : ℕ} (a : Fin n) :

Fin.succ (Fin.succ a) ≠ 1

source

ink

def Fin.castLt {n : ℕ} {m : ℕ} (i : Fin m) (h : ↑i < n) :

Fin n

castLt i h embeds i into a Fin where h proves it belongs into.

Equations

Fin.castLt i h = { val := ↑i, isLt := h }

source

ink

@[simp]

theorem Fin.coe_castLt {n : ℕ} {m : ℕ} (i : Fin m) (h : ↑i < n) :

↑(Fin.castLt i h) = ↑i

source

ink

@[simp]

theorem Fin.castLt_mk (i : ℕ) (n : ℕ) (m : ℕ) (hn : i < n) (hm : i < m) :

Fin.castLt { val := i, isLt := hn } hm = { val := i, isLt := hm }

source

ink

def Fin.castLe {n : ℕ} {m : ℕ} (h : n ≤ m) :

Fin n ↪o Fin m

castLe h i embeds i into a larger Fin type.

Equations

Fin.castLe h = OrderEmbedding.ofStrictMono (fun a => Fin.castLt a (_ : ↑a < m)) (_ : ∀ (x x_1 : Fin n), x < x_1 → x < x_1)

source

ink

@[simp]

theorem Fin.coe_castLe {n : ℕ} {m : ℕ} (h : n ≤ m) (i : Fin n) :

↑(↑(Fin.castLe h).toEmbedding i) = ↑i

source

ink

@[simp]

theorem Fin.castLe_mk (i : ℕ) (n : ℕ) (m : ℕ) (hn : i < n) (h : n ≤ m) :

↑(Fin.castLe h).toEmbedding { val := i, isLt := hn } = { val := i, isLt := (_ : i < m) }

source

ink

@[simp]

theorem Fin.castLe_zero {n : ℕ} {m : ℕ} (h : Nat.succ n ≤ Nat.succ m) :

↑(Fin.castLe h).toEmbedding 0 = 0

source

ink

@[simp]

theorem Fin.range_castLe {n : ℕ} {k : ℕ} (h : n ≤ k) :

Set.range ↑(Fin.castLe h).toEmbedding = { i | ↑i < n }

source

ink

@[simp]

theorem Fin.coe_of_injective_castLe_symm {n : ℕ} {k : ℕ} (h : n ≤ k) (i : Fin k) (hi : i ∈ Set.range ↑(Fin.castLe h).toEmbedding) :

↑(↑(Equiv.symm (Equiv.ofInjective ↑(Fin.castLe h).toEmbedding (_ : Function.Injective ↑(Fin.castLe h).toEmbedding))) { val := i, property := hi }) = ↑i

source

ink

@[simp]

theorem Fin.castLe_succ {m : ℕ} {n : ℕ} (h : m + 1 ≤ n + 1) (i : Fin m) :

↑(Fin.castLe h).toEmbedding (Fin.succ i) = Fin.succ (↑(Fin.castLe (_ : m ≤ n)).toEmbedding i)

source

ink

@[simp]

theorem Fin.castLe_castLe {k : ℕ} {m : ℕ} {n : ℕ} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :

↑(Fin.castLe mn).toEmbedding (↑(Fin.castLe km).toEmbedding i) = ↑(Fin.castLe (_ : k ≤ n)).toEmbedding i

source

ink

@[simp]

theorem Fin.castLe_comp_castLe {k : ℕ} {m : ℕ} {n : ℕ} (km : k ≤ m) (mn : m ≤ n) :

↑(Fin.castLe mn).toEmbedding ∘ ↑(Fin.castLe km).toEmbedding = ↑(Fin.castLe (_ : k ≤ n)).toEmbedding

source

ink

def Fin.cast {n : ℕ} {m : ℕ} (eq : n = m) :

Fin n ≃o Fin m

cast eq i embeds i into a equal Fin type, see also Equiv.finCongr.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Fin.symm_cast {n : ℕ} {m : ℕ} (h : n = m) :

OrderIso.symm (Fin.cast h) = Fin.cast (_ : m = n)

source

ink

theorem Fin.coe_cast {n : ℕ} {m : ℕ} (h : n = m) (i : Fin n) :

↑(↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding i) = ↑i

source

ink

@[simp]

theorem Fin.cast_zero {n : ℕ} {n' : ℕ} [inst : NeZero n] {h : n = n'} :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding 0 = 0

source

ink

@[simp]

theorem Fin.cast_last {n : ℕ} {n' : ℕ} {h : n + 1 = n' + 1} :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (Fin.last n) = Fin.last n'

source

ink

@[simp]

theorem Fin.cast_mk {n : ℕ} {m : ℕ} (h : n = m) (i : ℕ) (hn : i < n) :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding { val := i, isLt := hn } = { val := i, isLt := (_ : i < m) }

source

ink

@[simp]

theorem Fin.cast_trans {n : ℕ} {m : ℕ} {k : ℕ} (h : n = m) (h' : m = k) {i : Fin n} :

↑(RelIso.toRelEmbedding (Fin.cast h')).toEmbedding (↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : n = k))).toEmbedding i

source

ink

@[simp]

theorem Fin.cast_refl {n : ℕ} (h : optParam (n = n) (_ : n = n)) :

Fin.cast h = OrderIso.refl (Fin n)

source

ink

theorem Fin.castLe_of_eq {m : ℕ} {n : ℕ} (h : m = n) {h' : m ≤ n} :

↑(Fin.castLe h').toEmbedding = ↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding

source

ink

theorem Fin.cast_to_equiv {n : ℕ} {m : ℕ} (h : n = m) :

(Fin.cast h).toEquiv = Equiv.cast (_ : Fin n = Fin m)

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

source

ink

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

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding = ↑(RelIso.toRelEmbedding (Fin.cast (_ : n = m))).toEmbedding

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

source

ink

def Fin.castAdd {n : ℕ} (m : ℕ) :

Fin n ↪o Fin (n + m)

castAdd m i embeds i : Fin n in Fin (n+m). See also Fin.natAdd and Fin.addNat.

Equations

Fin.castAdd m = Fin.castLe (_ : n ≤ n + m)

source

ink

@[simp]

theorem Fin.coe_castAdd {n : ℕ} (m : ℕ) (i : Fin n) :

↑(↑(Fin.castAdd m).toEmbedding i) = ↑i

source

ink

@[simp]

theorem Fin.castAdd_zero {n : ℕ} :

↑(Fin.castAdd 0).toEmbedding = ↑(RelIso.toRelEmbedding (Fin.cast (_ : n = n))).toEmbedding

source

ink

theorem Fin.castAdd_lt {m : ℕ} (n : ℕ) (i : Fin m) :

↑(↑(Fin.castAdd n).toEmbedding i) < m

source

ink

@[simp]

theorem Fin.castAdd_mk {n : ℕ} (m : ℕ) (i : ℕ) (h : i < n) :

↑(Fin.castAdd m).toEmbedding { val := i, isLt := h } = { val := i, isLt := (_ : i < n + m) }

source

ink

@[simp]

theorem Fin.castAdd_castLt {n : ℕ} (m : ℕ) (i : Fin (n + m)) (hi : ↑i < n) :

↑(Fin.castAdd m).toEmbedding (Fin.castLt i hi) = i

source

ink

@[simp]

theorem Fin.castLt_castAdd {n : ℕ} (m : ℕ) (i : Fin n) :

Fin.castLt (↑(Fin.castAdd m).toEmbedding i) (_ : ↑(↑(Fin.castAdd m).toEmbedding i) < n) = i

source

ink

theorem Fin.castAdd_cast {n : ℕ} {n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n) :

↑(Fin.castAdd m).toEmbedding (↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : n' + m = n + m))).toEmbedding (↑(Fin.castAdd m).toEmbedding i)

For rewriting in the reverse direction, see Fin.cast_castAdd_left.

source

ink

theorem Fin.cast_castAdd_left {n : ℕ} {n' : ℕ} {m : ℕ} (i : Fin n') (h : n' + m = n + m) :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (↑(Fin.castAdd m).toEmbedding i) = ↑(Fin.castAdd m).toEmbedding (↑(RelIso.toRelEmbedding (Fin.cast (_ : n' = n))).toEmbedding i)

source

ink

@[simp]

theorem Fin.cast_castAdd_right {n : ℕ} {m : ℕ} {m' : ℕ} (i : Fin n) (h : n + m' = n + m) :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (↑(Fin.castAdd m').toEmbedding i) = ↑(Fin.castAdd m).toEmbedding i

source

ink

theorem Fin.castAdd_castAdd {m : ℕ} {n : ℕ} {p : ℕ} (i : Fin m) :

↑(Fin.castAdd p).toEmbedding (↑(Fin.castAdd n).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : m + (n + p) = m + n + p))).toEmbedding (↑(Fin.castAdd (n + p)).toEmbedding i)

source

ink

@[simp]

theorem Fin.cast_succ_eq {n : ℕ} {n' : ℕ} (i : Fin n) (h : Nat.succ n = Nat.succ n') :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (Fin.succ i) = Fin.succ (↑(RelIso.toRelEmbedding (Fin.cast (_ : n = n'))).toEmbedding i)

The cast of the successor is the succesor of the cast. See Fin.succ_cast_eq for rewriting in the reverse direction.

source

ink

theorem Fin.succ_cast_eq {n : ℕ} {n' : ℕ} (i : Fin n) (h : n = n') :

Fin.succ (↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : Nat.succ n = Nat.succ n'))).toEmbedding (Fin.succ i)

source

ink

def Fin.castSucc {n : ℕ} :

Fin n ↪o Fin (n + 1)

castSucc i embeds i : Fin n in Fin (n+1).

Equations

Fin.castSucc = Fin.castAdd 1

source

ink

@[simp]

theorem Fin.coe_castSucc {n : ℕ} (i : Fin n) :

↑(↑Fin.castSucc.toEmbedding i) = ↑i

source

ink

@[simp]

theorem Fin.castSucc_mk (n : ℕ) (i : ℕ) (h : i < n) :

↑Fin.castSucc.toEmbedding { val := i, isLt := h } = { val := i, isLt := (_ : i < Nat.succ n) }

source

ink

@[simp]

theorem Fin.cast_castSucc {n : ℕ} {n' : ℕ} {h : n + 1 = n' + 1} {i : Fin n} :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (↑Fin.castSucc.toEmbedding i) = ↑Fin.castSucc.toEmbedding (↑(RelIso.toRelEmbedding (Fin.cast (_ : n = n'))).toEmbedding i)

source

ink

theorem Fin.castSucc_lt_succ {n : ℕ} (i : Fin n) :

↑Fin.castSucc.toEmbedding i < Fin.succ i

source

ink

theorem Fin.le_castSucc_iff {n : ℕ} {i : Fin (n + 1)} {j : Fin n} :

i ≤ ↑Fin.castSucc.toEmbedding j ↔ i < Fin.succ j

source

ink

theorem Fin.castSucc_lt_iff_succ_le {n : ℕ} {i : Fin n} {j : Fin (n + 1)} :

↑Fin.castSucc.toEmbedding i < j ↔ Fin.succ i ≤ j

source

ink

@[simp]

theorem Fin.succ_last (n : ℕ) :

Fin.succ (Fin.last n) = Fin.last (Nat.succ n)

source

ink

@[simp]

theorem Fin.succ_eq_last_succ {n : ℕ} (i : Fin (Nat.succ n)) :

Fin.succ i = Fin.last (n + 1) ↔ i = Fin.last n

source

ink

@[simp]

theorem Fin.castSucc_cast_lt {n : ℕ} (i : Fin (n + 1)) (h : ↑i < n) :

↑Fin.castSucc.toEmbedding (Fin.castLt i h) = i

source

ink

@[simp]

theorem Fin.cast_lt_castSucc {n : ℕ} (a : Fin n) (h : ↑a < n) :

Fin.castLt (↑Fin.castSucc.toEmbedding a) h = a

source

ink

@[simp]

theorem Fin.castSucc_lt_castSucc_iff {n : ℕ} {a : Fin n} {b : Fin n} :

↑Fin.castSucc.toEmbedding a < ↑Fin.castSucc.toEmbedding b ↔ a < b

source

ink

theorem Fin.castSucc_injective (n : ℕ) :

Function.Injective ↑Fin.castSucc.toEmbedding

source

ink

theorem Fin.castSucc_inj {n : ℕ} {a : Fin n} {b : Fin n} :

↑Fin.castSucc.toEmbedding a = ↑Fin.castSucc.toEmbedding b ↔ a = b

source

ink

theorem Fin.castSucc_lt_last {n : ℕ} (a : Fin n) :

↑Fin.castSucc.toEmbedding a < Fin.last n

source

ink

@[simp]

theorem Fin.castSucc_zero {n : ℕ} [inst : NeZero n] :

↑Fin.castSucc.toEmbedding 0 = 0

source

ink

@[simp]

theorem Fin.castSucc_one {n : ℕ} :

↑Fin.castSucc.toEmbedding 1 = 1

source

ink

theorem Fin.castSucc_pos {n : ℕ} [inst : NeZero n] {i : Fin n} (h : 0 < i) :

0 < ↑Fin.castSucc.toEmbedding i

castSucc i is positive when i is positive

source

ink

@[simp]

theorem Fin.castSucc_eq_zero_iff {n : ℕ} [inst : NeZero n] (a : Fin n) :

↑Fin.castSucc.toEmbedding a = 0 ↔ a = 0

source

ink

theorem Fin.castSucc_ne_zero_iff {n : ℕ} [inst : NeZero n] (a : Fin n) :

↑Fin.castSucc.toEmbedding a ≠ 0 ↔ a ≠ 0

source

ink

theorem Fin.castSucc_fin_succ (n : ℕ) (j : Fin n) :

↑Fin.castSucc.toEmbedding (Fin.succ j) = Fin.succ (↑Fin.castSucc.toEmbedding j)

source

ink

@[simp]

theorem Fin.coe_eq_castSucc {n : ℕ} {a : Fin n} :

↑↑a = ↑Fin.castSucc.toEmbedding a

source

ink

@[simp]

theorem Fin.coeSucc_eq_succ {n : ℕ} {a : Fin n} :

↑Fin.castSucc.toEmbedding a + 1 = Fin.succ a

source

ink

theorem Fin.lt_succ {n : ℕ} {a : Fin n} :

↑Fin.castSucc.toEmbedding a < Fin.succ a

source

ink

@[simp]

theorem Fin.range_castSucc {n : ℕ} :

Set.range ↑Fin.castSucc.toEmbedding = { i | ↑i < n }

source

ink

theorem Fin.exists_castSucc_eq {n : ℕ} {i : Fin (n + 1)} :

(∃ j, ↑Fin.castSucc.toEmbedding j = i) ↔ i ≠ Fin.last n

source

ink

@[simp]

theorem Fin.coe_of_injective_castSucc_symm {n : ℕ} (i : Fin (Nat.succ n)) (hi : i ∈ Set.range ↑Fin.castSucc.toEmbedding) :

↑(↑(Equiv.symm (Equiv.ofInjective ↑Fin.castSucc.toEmbedding (_ : Function.Injective ↑Fin.castSucc.toEmbedding))) { val := i, property := hi }) = ↑i

source

ink

theorem Fin.succ_castSucc {n : ℕ} (i : Fin n) :

Fin.succ (↑Fin.castSucc.toEmbedding i) = ↑Fin.castSucc.toEmbedding (Fin.succ i)

source

ink

def Fin.addNat {n : ℕ} (m : ℕ) :

Fin n ↪o Fin (n + m)

addNat m i adds m to i, generalizes Fin.succ.

Equations

Fin.addNat m = OrderEmbedding.ofStrictMono (fun i => { val := ↑i + m, isLt := (_ : ↑i + m < n + m) }) (_ : ∀ (i j : Fin n), i < j → ↑i + m < ↑j + m)

source

ink

@[simp]

theorem Fin.coe_addNat {n : ℕ} (m : ℕ) (i : Fin n) :

↑(↑(Fin.addNat m).toEmbedding i) = ↑i + m

source

ink

@[simp]

theorem Fin.addNat_one {n : ℕ} {i : Fin n} :

↑(Fin.addNat 1).toEmbedding i = Fin.succ i

source

ink

theorem Fin.le_coe_addNat {n : ℕ} (m : ℕ) (i : Fin n) :

m ≤ ↑(↑(Fin.addNat m).toEmbedding i)

source

ink

@[simp]

theorem Fin.addNat_mk {m : ℕ} (n : ℕ) (i : ℕ) (hi : i < m) :

↑(Fin.addNat n).toEmbedding { val := i, isLt := hi } = { val := i + n, isLt := (_ : i + n < m + n) }

source

ink

@[simp]

theorem Fin.cast_addNat_zero {n : ℕ} {n' : ℕ} (i : Fin n) (h : n + 0 = n') :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (↑(Fin.addNat 0).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : n = n'))).toEmbedding i

source

ink

theorem Fin.addNat_cast {n : ℕ} {n' : ℕ} {m : ℕ} (i : Fin n') (h : n' = n) :

↑(Fin.addNat m).toEmbedding (↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : n' + m = n + m))).toEmbedding (↑(Fin.addNat m).toEmbedding i)

For rewriting in the reverse direction, see Fin.cast_addNat_left.

source

ink

theorem Fin.cast_addNat_left {n : ℕ} {n' : ℕ} {m : ℕ} (i : Fin n') (h : n' + m = n + m) :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (↑(Fin.addNat m).toEmbedding i) = ↑(Fin.addNat m).toEmbedding (↑(RelIso.toRelEmbedding (Fin.cast (_ : n' = n))).toEmbedding i)

source

ink

@[simp]

theorem Fin.cast_addNat_right {n : ℕ} {m : ℕ} {m' : ℕ} (i : Fin n) (h : n + m' = n + m) :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (↑(Fin.addNat m').toEmbedding i) = ↑(Fin.addNat m).toEmbedding i

source

ink

def Fin.natAdd (n : ℕ) {m : ℕ} :

Fin m ↪o Fin (n + m)

natAdd n i adds n to i "on the left".

Equations

Fin.natAdd n = OrderEmbedding.ofStrictMono (fun i => { val := n + ↑i, isLt := (_ : n + ↑i < n + m) }) (_ : ∀ (i j : Fin m), i < j → n + ↑i < n + ↑j)

source

ink

@[simp]

theorem Fin.coe_natAdd (n : ℕ) {m : ℕ} (i : Fin m) :

↑(↑(Fin.natAdd n).toEmbedding i) = n + ↑i

source

ink

@[simp]

theorem Fin.natAdd_mk {m : ℕ} (n : ℕ) (i : ℕ) (hi : i < m) :

↑(Fin.natAdd n).toEmbedding { val := i, isLt := hi } = { val := n + i, isLt := (_ : n + i < n + m) }

source

ink

theorem Fin.le_coe_natAdd {n : ℕ} (m : ℕ) (i : Fin n) :

m ≤ ↑(↑(Fin.natAdd m).toEmbedding i)

source

ink

theorem Fin.natAdd_zero {n : ℕ} :

Fin.natAdd 0 = RelIso.toRelEmbedding (Fin.cast (_ : n = 0 + n))

source

ink

theorem Fin.natAdd_cast {n : ℕ} {n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n) :

↑(Fin.natAdd m).toEmbedding (↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : m + n' = m + n))).toEmbedding (↑(Fin.natAdd m).toEmbedding i)

For rewriting in the reverse direction, see Fin.cast_natAdd_right.

source

ink

theorem Fin.cast_natAdd_right {n : ℕ} {n' : ℕ} {m : ℕ} (i : Fin n') (h : m + n' = m + n) :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (↑(Fin.natAdd m).toEmbedding i) = ↑(Fin.natAdd m).toEmbedding (↑(RelIso.toRelEmbedding (Fin.cast (_ : n' = n))).toEmbedding i)

source

ink

@[simp]

theorem Fin.cast_natAdd_left {n : ℕ} {m : ℕ} {m' : ℕ} (i : Fin n) (h : m' + n = m + n) :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (↑(Fin.natAdd m').toEmbedding i) = ↑(Fin.natAdd m).toEmbedding i

source

ink

theorem Fin.castAdd_natAdd (p : ℕ) (m : ℕ) {n : ℕ} (i : Fin n) :

↑(Fin.castAdd p).toEmbedding (↑(Fin.natAdd m).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : m + (n + p) = m + n + p))).toEmbedding (↑(Fin.natAdd m).toEmbedding (↑(Fin.castAdd p).toEmbedding i))

source

ink

theorem Fin.natAdd_castAdd (p : ℕ) (m : ℕ) {n : ℕ} (i : Fin n) :

↑(Fin.natAdd m).toEmbedding (↑(Fin.castAdd p).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : m + n + p = m + (n + p)))).toEmbedding (↑(Fin.castAdd p).toEmbedding (↑(Fin.natAdd m).toEmbedding i))

source

ink

theorem Fin.natAdd_natAdd (m : ℕ) (n : ℕ) {p : ℕ} (i : Fin p) :

↑(Fin.natAdd m).toEmbedding (↑(Fin.natAdd n).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : m + n + p = m + (n + p)))).toEmbedding (↑(Fin.natAdd (m + n)).toEmbedding i)

source

ink

@[simp]

theorem Fin.cast_natAdd_zero {n : ℕ} {n' : ℕ} (i : Fin n) (h : 0 + n = n') :

↑(RelIso.toRelEmbedding (Fin.cast h)).toEmbedding (↑(Fin.natAdd 0).toEmbedding i) = ↑(RelIso.toRelEmbedding (Fin.cast (_ : n = n'))).toEmbedding i

source

ink

@[simp]

theorem Fin.cast_natAdd (n : ℕ) {m : ℕ} (i : Fin m) :

↑(RelIso.toRelEmbedding (Fin.cast (_ : n + m = m + n))).toEmbedding (↑(Fin.natAdd n).toEmbedding i) = ↑(Fin.addNat n).toEmbedding i

source

ink

@[simp]

theorem Fin.cast_addNat {n : ℕ} (m : ℕ) (i : Fin n) :

↑(RelIso.toRelEmbedding (Fin.cast (_ : n + m = m + n))).toEmbedding (↑(Fin.addNat m).toEmbedding i) = ↑(Fin.natAdd m).toEmbedding i

source

ink

@[simp]

theorem Fin.natAdd_last {m : ℕ} {n : ℕ} :

↑(Fin.natAdd n).toEmbedding (Fin.last m) = Fin.last (n + m)

source

ink

theorem Fin.natAdd_castSucc {m : ℕ} {n : ℕ} {i : Fin m} :

↑(Fin.natAdd n).toEmbedding (↑Fin.castSucc.toEmbedding i) = ↑Fin.castSucc.toEmbedding (↑(Fin.natAdd n).toEmbedding i)

pred #

source

ink

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

i ≠ 0 → Fin n

Predecessor

Equations

Fin.pred x x = match x, x with | { val := a, isLt := h₁ }, h₂ => { val := Nat.pred a, isLt := (_ : Nat.pred a < Nat.pred (n + 1)) }

source

ink

@[simp]

theorem Fin.coe_pred {n : ℕ} (j : Fin (n + 1)) (h : j ≠ 0) :

↑(Fin.pred j h) = ↑j - 1

source

ink

@[simp]

theorem Fin.succ_pred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ 0) :

Fin.succ (Fin.pred i h) = i

source

ink

@[simp]

theorem Fin.pred_succ {n : ℕ} (i : Fin n) {h : Fin.succ i ≠ 0} :

Fin.pred (Fin.succ i) h = i

source

ink

theorem Fin.pred_eq_iff_eq_succ {n : ℕ} (i : Fin (n + 1)) (hi : i ≠ 0) (j : Fin n) :

Fin.pred i hi = j ↔ i = Fin.succ j

source

ink

theorem Fin.pred_mk_succ {n : ℕ} (i : ℕ) (h : i < n + 1) :

Fin.pred { val := i + 1, isLt := (_ : i + 1 < n + 1 + 1) } (_ : { val := i + 1, isLt := (_ : i + 1 < n + 1 + 1) } ≠ 0) = { val := i, isLt := h }

source

ink

@[simp]

theorem Fin.pred_mk_succ' {n : ℕ} (i : ℕ) (h₁ : i + 1 < n + 1 + 1) (h₂ : { val := i + 1, isLt := h₁ } ≠ 0) :

Fin.pred { val := i + 1, isLt := h₁ } h₂ = { val := i, isLt := (_ : i < n + 1) }

source

ink

theorem Fin.pred_mk {n : ℕ} (i : ℕ) (h : i < n + 1) (w : { val := i, isLt := h } ≠ 0) :

Fin.pred { val := i, isLt := h } w = { val := i - 1, isLt := (_ : i - 1 < n) }

source

ink

@[simp]

theorem Fin.pred_le_pred_iff {n : ℕ} {a : Fin (Nat.succ n)} {b : Fin (Nat.succ n)} {ha : a ≠ 0} {hb : b ≠ 0} :

Fin.pred a ha ≤ Fin.pred b hb ↔ a ≤ b

source

ink

@[simp]

theorem Fin.pred_lt_pred_iff {n : ℕ} {a : Fin (Nat.succ n)} {b : Fin (Nat.succ n)} {ha : a ≠ 0} {hb : b ≠ 0} :

Fin.pred a ha < Fin.pred b hb ↔ a < b

source

ink

@[simp]

theorem Fin.pred_inj {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0} :

Fin.pred a ha = Fin.pred b hb ↔ a = b

source

ink

@[simp]

theorem Fin.pred_one {n : ℕ} :

Fin.pred 1 (_ : 1 ≠ 0) = 0

source

ink

theorem Fin.pred_add_one {n : ℕ} (i : Fin (n + 2)) (h : ↑i < n + 1) :

Fin.pred (i + 1) (_ : i + 1 ≠ 0) = Fin.castLt i h

source

ink

def Fin.subNat {n : ℕ} (m : ℕ) (i : Fin (n + m)) (h : m ≤ ↑i) :

Fin n

subNat i h subtracts m from i, generalizes Fin.pred.

Equations

Fin.subNat m i h = { val := ↑i - m, isLt := (_ : ↑i - m < n) }

source

ink

@[simp]

theorem Fin.coe_subNat {n : ℕ} {m : ℕ} (i : Fin (n + m)) (h : m ≤ ↑i) :

↑(Fin.subNat m i h) = ↑i - m

source

ink

@[simp]

theorem Fin.subNat_mk {n : ℕ} {m : ℕ} {i : ℕ} (h₁ : i < n + m) (h₂ : m ≤ i) :

Fin.subNat m { val := i, isLt := h₁ } h₂ = { val := i - m, isLt := (_ : i - m < n) }

source

ink

@[simp]

theorem Fin.pred_castSucc_succ {n : ℕ} (i : Fin n) :

Fin.pred (↑Fin.castSucc.toEmbedding (Fin.succ i)) (_ : ↑Fin.castSucc.toEmbedding (Fin.succ i) ≠ 0) = ↑Fin.castSucc.toEmbedding i

source

ink

@[simp]

theorem Fin.addNat_subNat {n : ℕ} {m : ℕ} {i : Fin (n + m)} (h : m ≤ ↑i) :

↑(Fin.addNat m).toEmbedding (Fin.subNat m i h) = i

source

ink

@[simp]

theorem Fin.subNat_addNat {n : ℕ} (i : Fin n) (m : ℕ) (h : optParam (m ≤ ↑(↑(Fin.addNat m).toEmbedding i)) (_ : m ≤ ↑(↑(Fin.addNat m).toEmbedding i))) :

Fin.subNat m (↑(Fin.addNat m).toEmbedding i) h = i

source

ink

@[simp]

theorem Fin.natAdd_subNat_cast {n : ℕ} {m : ℕ} {i : Fin (n + m)} (h : n ≤ ↑i) :

↑(Fin.natAdd n).toEmbedding (Fin.subNat n (↑(RelIso.toRelEmbedding (Fin.cast (_ : n + m = m + n))).toEmbedding i) h) = i

source

ink

def Fin.divNat {n : ℕ} {m : ℕ} (i : Fin (m * n)) :

Fin m

Compute i / n, where n is a Nat and inferred the type of i.

Equations

Fin.divNat i = { val := ↑i / n, isLt := (_ : ↑i / n < m) }

source

ink

@[simp]

theorem Fin.coe_divNat {n : ℕ} {m : ℕ} (i : Fin (m * n)) :

↑(Fin.divNat i) = ↑i / n

source

ink

def Fin.modNat {n : ℕ} {m : ℕ} (i : Fin (m * n)) :

Fin n

Compute i % n, where n is a Nat and inferred the type of i.

Equations

Fin.modNat i = { val := ↑i % n, isLt := (_ : ↑i % n < n) }

source

ink

@[simp]

theorem Fin.coe_modNat {n : ℕ} {m : ℕ} (i : Fin (m * n)) :

↑(Fin.modNat i) = ↑i % n

recursion and induction principles #

source

ink

def Fin.succRec {C : (n : ℕ) → Fin n → Sort u_1} (H0 : (n : ℕ) → C (Nat.succ n) 0) (Hs : (n : ℕ) → (i : Fin n) → C n i → C (Nat.succ n) (Fin.succ i)) {n : ℕ} (i : Fin n) :

C n i

Define C n i by induction on i : Fin n interpreted as (0 : Fin (n - i)).succ.succ…. This function has two arguments: H0 n defines 0-th element C (n+1) 0 of an (n+1)-tuple, and Hs n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.

Equations

Fin.succRec H0 Hs i = Fin.elim0 i
Fin.succRec H0 Hs { val := 0, isLt := isLt } = Eq.mpr (_ : C (Nat.succ n) { val := 0, isLt := isLt } = C (Nat.succ n) 0) (H0 n)
Fin.succRec H0 Hs { val := Nat.succ i, isLt := h } = Hs n { val := i, isLt := (_ : i < n) } (Fin.succRec H0 Hs { val := i, isLt := (_ : i < n) })

source

ink

def Fin.succRecOn {n : ℕ} (i : Fin n) {C : (n : ℕ) → Fin n → Sort u_1} (H0 : (n : ℕ) → C (n + 1) 0) (Hs : (n : ℕ) → (i : Fin n) → C n i → C (Nat.succ n) (Fin.succ i)) :

C n i

A version of Fin.succRec taking i : Fin n as the first argument.

Equations

Fin.succRecOn i H0 Hs = Fin.succRec H0 Hs i

source

ink

@[simp]

theorem Fin.succRecOn_zero {C : (n : ℕ) → Fin n → Sort u_1} {H0 : (n : ℕ) → C (n + 1) 0} {Hs : (n : ℕ) → (i : Fin n) → C n i → C (Nat.succ n) (Fin.succ i)} (n : ℕ) :

Fin.succRecOn 0 H0 Hs = H0 n

source

ink

@[simp]

theorem Fin.succRecOn_succ {C : (n : ℕ) → Fin n → Sort u_1} {H0 : (n : ℕ) → C (n + 1) 0} {Hs : (n : ℕ) → (i : Fin n) → C n i → C (Nat.succ n) (Fin.succ i)} {n : ℕ} (i : Fin n) :

Fin.succRecOn (Fin.succ i) H0 Hs = Hs n i (Fin.succRecOn i H0 Hs)

source

ink

def Fin.induction {n : ℕ} {C : Fin (n + 1) → Sort u_1} (h0 : C 0) (hs : (i : Fin n) → C (↑Fin.castSucc.toEmbedding i) → C (Fin.succ i)) (i : Fin (n + 1)) :

C i

Define C i by induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: h0 handles the base case on C 0, and hs defines the inductive step using C i.castSucc.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Fin.induction_zero {n : ℕ} {C : Fin (n + 1) → Sort u_1} (h0 : C 0) (hs : (i : Fin n) → C (↑Fin.castSucc.toEmbedding i) → C (Fin.succ i)) :

(fun i => Fin.induction h0 hs i) 0 = h0

source

ink

@[simp]

theorem Fin.induction_succ {n : ℕ} {C : Fin (n + 1) → Sort u_1} (h0 : C 0) (hs : (i : Fin n) → C (↑Fin.castSucc.toEmbedding i) → C (Fin.succ i)) (i : Fin n) :

(fun i => Fin.induction h0 hs i) (Fin.succ i) = hs i (Fin.induction h0 hs (↑Fin.castSucc.toEmbedding i))

source

ink

def Fin.inductionOn {n : ℕ} (i : Fin (n + 1)) {C : Fin (n + 1) → Sort u_1} (h0 : C 0) (hs : (i : Fin n) → C (↑Fin.castSucc.toEmbedding i) → C (Fin.succ i)) :

C i

A version of Fin.induction taking i : Fin (n + 1) as the first argument.

Equations

Fin.inductionOn i h0 hs = Fin.induction h0 hs i

source

ink

def Fin.cases {n : ℕ} {C : Fin (n + 1) → Sort u_1} (H0 : C 0) (Hs : (i : Fin n) → C (Fin.succ i)) (i : Fin (n + 1)) :

C i

Define f : Π i : Fin n.succ, C i by separately handling the cases i = 0 and i = j.succ, j : Fin n.

Equations

Fin.cases H0 Hs i = Fin.induction H0 (fun i x => Hs i) i

source

ink

@[simp]

theorem Fin.cases_zero {n : ℕ} {C : Fin (n + 1) → Sort u_1} {H0 : C 0} {Hs : (i : Fin n) → C (Fin.succ i)} :

Fin.cases H0 Hs 0 = H0

source

ink

@[simp]

theorem Fin.cases_succ {n : ℕ} {C : Fin (n + 1) → Sort u_1} {H0 : C 0} {Hs : (i : Fin n) → C (Fin.succ i)} (i : Fin n) :

Fin.cases H0 Hs (Fin.succ i) = Hs i

source

ink

@[simp]

theorem Fin.cases_succ' {n : ℕ} {C : Fin (n + 1) → Sort u_1} {H0 : C 0} {Hs : (i : Fin n) → C (Fin.succ i)} {i : ℕ} (h : i + 1 < n + 1) :

Fin.cases H0 Hs { val := Nat.succ i, isLt := h } = Hs { val := i, isLt := (_ : i < n) }

source

ink

theorem Fin.forall_fin_succ {n : ℕ} {P : Fin (n + 1) → Prop} :

((i : Fin (n + 1)) → P i) ↔ P 0 ∧ ((i : Fin n) → P (Fin.succ i))

source

ink

theorem Fin.exists_fin_succ {n : ℕ} {P : Fin (n + 1) → Prop} :

(∃ i, P i) ↔ P 0 ∨ ∃ i, P (Fin.succ i)

source

ink

theorem Fin.forall_fin_one {p : Fin 1 → Prop} :

((i : Fin 1) → p i) ↔ p 0

source

ink

theorem Fin.exists_fin_one {p : Fin 1 → Prop} :

(∃ i, p i) ↔ p 0

source

ink

theorem Fin.forall_fin_two {p : Fin 2 → Prop} :

((i : Fin 2) → p i) ↔ p 0 ∧ p 1

source

ink

theorem Fin.exists_fin_two {p : Fin 2 → Prop} :

(∃ i, p i) ↔ p 0 ∨ p 1

source

ink

theorem Fin.fin_two_eq_of_eq_zero_iff {a : Fin 2} {b : Fin 2} (h : a = 0 ↔ b = 0) :

a = b

source

ink

def Fin.reverseInduction {n : ℕ} {C : Fin (n + 1) → Sort u_1} (hlast : C (Fin.last n)) (hs : (i : Fin n) → C (Fin.succ i) → C (↑Fin.castSucc.toEmbedding i)) (i : Fin (n + 1)) :

C i

Define C i by reverse induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: hlast handles the base case on C (Fin.last n), and hs defines the inductive step using C i.succ, inducting downwards.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Fin.reverse_induction_last {n : ℕ} {C : Fin (n + 1) → Sort u_1} (h0 : C (Fin.last n)) (hs : (i : Fin n) → C (Fin.succ i) → C (↑Fin.castSucc.toEmbedding i)) :

Fin.reverseInduction h0 hs (Fin.last n) = h0

source

ink

@[simp]

theorem Fin.reverse_induction_castSucc {n : ℕ} {C : Fin (n + 1) → Sort u_1} (h0 : C (Fin.last n)) (hs : (i : Fin n) → C (Fin.succ i) → C (↑Fin.castSucc.toEmbedding i)) (i : Fin n) :

Fin.reverseInduction h0 hs (↑Fin.castSucc.toEmbedding i) = hs i (Fin.reverseInduction h0 hs (Fin.succ i))

source

ink

def Fin.lastCases {n : ℕ} {C : Fin (n + 1) → Sort u_1} (hlast : C (Fin.last n)) (hcast : (i : Fin n) → C (↑Fin.castSucc.toEmbedding i)) (i : Fin (n + 1)) :

C i

Define f : Π i : Fin n.succ, C i by separately handling the cases i = Fin.last n and i = j.castSucc, j : Fin n.

Equations

Fin.lastCases hlast hcast i = Fin.reverseInduction hlast (fun i x => hcast i) i

source

ink

@[simp]

theorem Fin.lastCases_last {n : ℕ} {C : Fin (n + 1) → Sort u_1} (hlast : C (Fin.last n)) (hcast : (i : Fin n) → C (↑Fin.castSucc.toEmbedding i)) :

Fin.lastCases hlast hcast (Fin.last n) = hlast

source

ink

@[simp]

theorem Fin.lastCases_castSucc {n : ℕ} {C : Fin (n + 1) → Sort u_1} (hlast : C (Fin.last n)) (hcast : (i : Fin n) → C (↑Fin.castSucc.toEmbedding i)) (i : Fin n) :

Fin.lastCases hlast hcast (↑Fin.castSucc.toEmbedding i) = hcast i

source

ink

def Fin.addCases {m : ℕ} {n : ℕ} {C : Fin (m + n) → Sort u} (hleft : (i : Fin m) → C (↑(Fin.castAdd n).toEmbedding i)) (hright : (i : Fin n) → C (↑(Fin.natAdd m).toEmbedding i)) (i : Fin (m + n)) :

C i

Define f : Π i : Fin (m + n), C i by separately handling the cases i = castAdd n i, j : Fin m and i = natAdd m j, j : Fin n.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Fin.addCases_left {m : ℕ} {n : ℕ} {C : Fin (m + n) → Sort u_1} (hleft : (i : Fin m) → C (↑(Fin.castAdd n).toEmbedding i)) (hright : (i : Fin n) → C (↑(Fin.natAdd m).toEmbedding i)) (i : Fin m) :

Fin.addCases hleft hright (↑(Fin.castAdd n).toEmbedding i) = hleft i

source

ink

@[simp]

theorem Fin.addCases_right {m : ℕ} {n : ℕ} {C : Fin (m + n) → Sort u_1} (hleft : (i : Fin m) → C (↑(Fin.castAdd n).toEmbedding i)) (hright : (i : Fin n) → C (↑(Fin.natAdd m).toEmbedding i)) (i : Fin n) :

Fin.addCases hleft hright (↑(Fin.natAdd m).toEmbedding i) = hright i

source

ink

theorem Fin.lift_fun_iff_succ {n : ℕ} {α : Type u_1} (r : α → α → Prop) [inst : IsTrans α r] {f : Fin (n + 1) → α} :

((fun x x_1 => x < x_1) ⇒ r) f f ↔ (i : Fin n) → r (f (↑Fin.castSucc.toEmbedding i)) (f (Fin.succ i))

source

ink

theorem Fin.strictMono_iff_lt_succ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α} :

StrictMono f ↔ ∀ (i : Fin n), f (↑Fin.castSucc.toEmbedding i) < f (Fin.succ i)

A function f on Fin (n + 1) is strictly monotone if and only if f i < f (i + 1) for all i.

source

ink

theorem Fin.monotone_iff_le_succ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α} :

Monotone f ↔ ∀ (i : Fin n), f (↑Fin.castSucc.toEmbedding i) ≤ f (Fin.succ i)

A function f on Fin (n + 1) is monotone if and only if f i ≤ f (i + 1) for all i.

source

ink

theorem Fin.strictAnti_iff_succ_lt {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α} :

StrictAnti f ↔ ∀ (i : Fin n), f (Fin.succ i) < f (↑Fin.castSucc.toEmbedding i)

A function f on Fin (n + 1) is strictly antitone if and only if f (i + 1) < f i for all i.

source

ink

theorem Fin.antitone_iff_succ_le {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α} :

Antitone f ↔ ∀ (i : Fin n), f (Fin.succ i) ≤ f (↑Fin.castSucc.toEmbedding i)

A function f on Fin (n + 1) is antitone if and only if f (i + 1) ≤ f i for all i.

source

ink

instance Fin.neg (n : ℕ) :

Neg (Fin n)

Negation on Fin n

Equations

Fin.neg n = { neg := fun a => { val := (n - ↑a) % n, isLt := (_ : (n - ↑a) % n < n) } }

source

ink

instance Fin.addCommGroup (n : ℕ) [inst : NeZero n] :

AddCommGroup (Fin n)

Abelian group structure on Fin n.

Equations

Fin.addCommGroup n = let src := Fin.addCommMonoid n; let src_1 := Fin.neg n; AddCommGroup.mk (_ : ∀ (a b : Fin n), a + b = b + a)

source

ink

theorem Fin.coe_neg {n : ℕ} (a : Fin n) :

↑(-a) = (n - ↑a) % n

source

ink

theorem Fin.coe_sub {n : ℕ} (a : Fin n) (b : Fin n) :

↑(a - b) = (↑a + (n - ↑b)) % n

source

ink

theorem Fin.fin_one_eq_zero (a : Fin 1) :

a = 0

source

ink

@[simp]

theorem Fin.coe_fin_one (a : Fin 1) :

↑a = 0

source

ink

@[simp]

theorem Fin.coe_neg_one {n : ℕ} :

↑(-1) = n

source

ink

theorem Fin.coe_sub_one {n : ℕ} (a : Fin (n + 1)) :

↑(a - 1) = if a = 0 then n else ↑a - 1

source

ink

theorem Fin.coe_sub_iff_le {n : ℕ} {a : Fin n} {b : Fin n} :

↑(a - b) = ↑a - ↑b ↔ b ≤ a

source

ink

theorem Fin.coe_sub_iff_lt {n : ℕ} {a : Fin n} {b : Fin n} :

↑(a - b) = n + ↑a - ↑b ↔ a < b

source

ink

@[simp]

theorem Fin.lt_sub_one_iff {n : ℕ} {k : Fin (n + 2)} :

k < k - 1 ↔ k = 0

source

ink

@[simp]

theorem Fin.le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} :

k ≤ k - 1 ↔ k = 0

source

ink

@[simp]

theorem Fin.sub_one_lt_iff {n : ℕ} {k : Fin (n + 1)} :

k - 1 < k ↔ 0 < k

source

ink

theorem Fin.last_sub {n : ℕ} (i : Fin (n + 1)) :

Fin.last n - i = ↑Fin.rev i

source

ink

theorem Fin.succAbove_aux {n : ℕ} (p : Fin (n + 1)) :

StrictMono fun i => if ↑Fin.castSucc.toEmbedding i < p then ↑Fin.castSucc.toEmbedding i else Fin.succ i

source

ink

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

Fin n ↪o Fin (n + 1)

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

Equations

One or more equations did not get rendered due to their size.

source

ink

theorem Fin.succAbove_below {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : ↑Fin.castSucc.toEmbedding i < p) :

↑(Fin.succAbove p).toEmbedding i = ↑Fin.castSucc.toEmbedding 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.

source

ink

@[simp]

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

↑(Fin.succAbove a).toEmbedding 0 = 0

source

ink

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

↑(Fin.succAbove a).toEmbedding b = 0 ↔ b = 0

source

ink

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

↑(Fin.succAbove a).toEmbedding b ≠ 0

source

ink

@[simp]

theorem Fin.succAbove_zero {n : ℕ} :

↑(Fin.succAbove 0).toEmbedding = Fin.succ

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

source

ink

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

source

ink

theorem Fin.succAbove_last_apply {n : ℕ} (i : Fin n) :

↑(Fin.succAbove (Fin.last n)).toEmbedding i = ↑Fin.castSucc.toEmbedding i

source

ink

theorem Fin.succAbove_above {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p ≤ ↑Fin.castSucc.toEmbedding i) :

↑(Fin.succAbove p).toEmbedding 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.

source

ink

theorem Fin.succAbove_lt_ge {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :

↑Fin.castSucc.toEmbedding i < p ∨ p ≤ ↑Fin.castSucc.toEmbedding i

Embedding i : Fin n into Fin (n + 1) is always about some hole p.

source

ink

theorem Fin.succAbove_lt_gt {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :

↑Fin.castSucc.toEmbedding i < p ∨ p < Fin.succ i

Embedding i : Fin n into Fin (n + 1) is always about some hole p.

source

ink

@[simp]

theorem Fin.succAbove_lt_iff {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :

↑(Fin.succAbove p).toEmbedding i < p ↔ ↑Fin.castSucc.toEmbedding 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.

source

ink

theorem Fin.lt_succAbove_iff {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :

p < ↑(Fin.succAbove p).toEmbedding i ↔ p ≤ ↑Fin.castSucc.toEmbedding 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.

source

ink

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

↑(Fin.succAbove p).toEmbedding i ≠ p

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

source

ink

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

0 < ↑(Fin.succAbove p).toEmbedding i

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

source

ink

@[simp]

theorem Fin.succAbove_castLt {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x < y) (hx : optParam (↑x < n) (_ : ↑x < n)) :

↑(Fin.succAbove y).toEmbedding (Fin.castLt x hx) = x

source

ink

@[simp]

theorem Fin.succAbove_pred {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x < y) (hy : optParam (y ≠ 0) (_ : y ≠ 0)) :

↑(Fin.succAbove x).toEmbedding (Fin.pred y hy) = y

source

ink

theorem Fin.castLt_succAbove {n : ℕ} {x : Fin n} {y : Fin (n + 1)} (h : ↑Fin.castSucc.toEmbedding x < y) (h' : optParam (↑(↑(Fin.succAbove y).toEmbedding x) < n) (_ : ↑(↑(Fin.succAbove y).toEmbedding x) < n)) :

Fin.castLt (↑(Fin.succAbove y).toEmbedding x) h' = x

source

ink

theorem Fin.pred_succAbove {n : ℕ} {x : Fin n} {y : Fin (n + 1)} (h : y ≤ ↑Fin.castSucc.toEmbedding x) (h' : optParam (↑(Fin.succAbove y).toEmbedding x ≠ 0) (_ : ↑(Fin.succAbove y).toEmbedding x ≠ 0)) :

Fin.pred (↑(Fin.succAbove y).toEmbedding x) h' = x

source

ink

theorem Fin.exists_succAbove_eq {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x ≠ y) :

∃ z, ↑(Fin.succAbove y).toEmbedding z = x

source

ink

@[simp]

theorem Fin.exists_succAbove_eq_iff {n : ℕ} {x : Fin (n + 1)} {y : Fin (n + 1)} :

(∃ z, ↑(Fin.succAbove x).toEmbedding z = y) ↔ y ≠ x

source

ink

@[simp]

theorem Fin.range_succAbove {n : ℕ} (p : Fin (n + 1)) :

Set.range ↑(Fin.succAbove p).toEmbedding = {p}ᶜ

The range of p.succAbove is everything except p.

source

ink

@[simp]

theorem Fin.range_succ (n : ℕ) :

Set.range Fin.succ = {0}ᶜ

source

ink

@[simp]

theorem Fin.exists_succ_eq_iff {n : ℕ} {x : Fin (n + 1)} :

(∃ y, Fin.succ y = x) ↔ x ≠ 0

source

ink

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

Function.Injective ↑(Fin.succAbove x).toEmbedding

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

source

ink

theorem Fin.succAbove_right_inj {n : ℕ} {a : Fin n} {b : Fin n} {x : Fin (n + 1)} :

↑(Fin.succAbove x).toEmbedding a = ↑(Fin.succAbove x).toEmbedding b ↔ a = b

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

source

ink

theorem Fin.succAbove_left_injective {n : ℕ} :

Function.Injective Fin.succAbove

succAbove is injective at the pivot

source

ink

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

source

ink

@[simp]

theorem Fin.zero_succAbove {n : ℕ} (i : Fin n) :

↑(Fin.succAbove 0).toEmbedding i = Fin.succ i

source

ink

@[simp]

theorem Fin.succ_succAbove_zero {n : ℕ} [inst : NeZero n] (i : Fin n) :

↑(Fin.succAbove (Fin.succ i)).toEmbedding 0 = 0

source

ink

@[simp]

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

↑(Fin.succAbove (Fin.succ i)).toEmbedding (Fin.succ j) = Fin.succ (↑(Fin.succAbove i).toEmbedding j)

source

ink

theorem Fin.one_succAbove_zero {n : ℕ} :

↑(Fin.succAbove 1).toEmbedding 0 = 0

source

ink

@[simp]

theorem Fin.succ_succAbove_one {n : ℕ} [inst : NeZero n] (i : Fin (n + 1)) :

↑(Fin.succAbove (Fin.succ i)).toEmbedding 1 = Fin.succ (↑(Fin.succAbove i).toEmbedding 0)

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

source

ink

@[simp]

theorem Fin.one_succAbove_succ {n : ℕ} (j : Fin n) :

↑(Fin.succAbove 1).toEmbedding (Fin.succ j) = Fin.succ (Fin.succ j)

source

ink

@[simp]

theorem Fin.one_succAbove_one {n : ℕ} :

↑(Fin.succAbove 1).toEmbedding 1 = 2

source

ink

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

Fin n

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

Equations

Fin.predAbove p i = if h : ↑Fin.castSucc.toEmbedding p < i then Fin.pred i (_ : i ≠ 0) else Fin.castLt i (_ : ↑i < n)

source

ink

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

Monotone (Fin.predAbove p)

source

ink

theorem Fin.predAbove_left_monotone {n : ℕ} (i : Fin (n + 1)) :

Monotone fun p => Fin.predAbove p i

source

ink

def Fin.castPred {n : ℕ} (i : Fin (n + 2)) :

Fin (n + 1)

castPred embeds i : Fin (n + 2) into Fin (n + 1) by lowering just last (n + 1) to last n.

Equations

Fin.castPred i = Fin.predAbove (Fin.last n) i

source

ink

@[simp]

theorem Fin.castPred_zero {n : ℕ} :

Fin.castPred 0 = 0

source

ink

@[simp]

theorem Fin.castPred_one {n : ℕ} :

Fin.castPred 1 = 1

source

ink

@[simp]

theorem Fin.predAbove_zero {n : ℕ} {i : Fin (n + 2)} (hi : i ≠ 0) :

Fin.predAbove 0 i = Fin.pred i hi

source

ink

@[simp]

theorem Fin.castPred_last {n : ℕ} :

Fin.castPred (Fin.last (n + 1)) = Fin.last n

source

ink

theorem Fin.castPred_mk (n : ℕ) (i : ℕ) (h : i < n + 1) :

Fin.castPred { val := i, isLt := (_ : i < Nat.succ (n + 1)) } = { val := i, isLt := h }

source

ink

@[simp]

theorem Fin.castPred_mk' (n : ℕ) (i : ℕ) (h₁ : i < n + 2) (h₂ : i < n + 1) :

Fin.castPred { val := i, isLt := h₁ } = { val := i, isLt := h₂ }

source

ink

theorem Fin.coe_castPred {n : ℕ} (a : Fin (n + 2)) (hx : a < Fin.last (n + 1)) :

↑(Fin.castPred a) = ↑a

source

ink

theorem Fin.predAbove_below {n : ℕ} (p : Fin (n + 1)) (i : Fin (n + 2)) (h : i ≤ ↑Fin.castSucc.toEmbedding p) :

Fin.predAbove p i = Fin.castPred i

source

ink

@[simp]

theorem Fin.predAbove_last {n : ℕ} :

Fin.predAbove (Fin.last n) = Fin.castPred

source

ink

theorem Fin.predAbove_last_apply {n : ℕ} (i : Fin n) :

Fin.predAbove (Fin.last n) ↑↑i = Fin.castPred ↑↑i

source

ink

theorem Fin.predAbove_above {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : ↑Fin.castSucc.toEmbedding p < i) :

Fin.predAbove p i = Fin.pred i (_ : i ≠ 0)

source

ink

theorem Fin.castPred_monotone {n : ℕ} :

Monotone Fin.castPred

source

ink

@[simp]

theorem Fin.succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ ↑Fin.castSucc.toEmbedding p) :

↑(Fin.succAbove (↑Fin.castSucc.toEmbedding p)).toEmbedding (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.

source

ink

@[simp]

theorem Fin.predAbove_succAbove {n : ℕ} (p : Fin n) (i : Fin n) :

Fin.predAbove p (↑(Fin.succAbove (↑Fin.castSucc.toEmbedding p)).toEmbedding 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

ink

theorem Fin.castSucc_pred_eq_pred_castSucc {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) (ha' : optParam (↑Fin.castSucc.toEmbedding a ≠ 0) (_ : ↑Fin.castSucc.toEmbedding a ≠ 0)) :

↑Fin.castSucc.toEmbedding (Fin.pred a ha) = Fin.pred (↑Fin.castSucc.toEmbedding a) ha'

source

ink

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).toEmbedding b ≠ 0) (_ : ↑(Fin.succAbove a).toEmbedding b ≠ 0)) :