Documentation

LeanPool.FoZfc.FixedSnoc

The version of Fin.snoc for the fixed type. #

Main Definitions #

Main Statements #

Implimentation notes #

source
def FirstOrder.ZFC.FixedSnoc.fixedSnoc {V : Type u} {n : ℕ} (xs : Fin n → V) (b : V) (k : Fin (n + 1)) :
V

Fin.snoc for the type V.

Equations
Instances For
    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.snoc_conv {V : Type u} {n : ℕ} {xs : Fin n → V} {b : V} :
    Fin.snoc xs b = fixedSnoc xs b

    Fin.snoc = fixedSnoc when applied to V.

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.snoc_last {V : Type u} {n : ℕ} (xs : Fin n → V) (a : V) :
    fixedSnoc xs a (Fin.last n) = a

    fixedSnoc xs a n = a when xs : Fin n → V

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.snoc_init {V : Type u} {n : ℕ} {xs : Fin n → V} {a : V} {k : Fin n} :
    fixedSnoc xs a k.castSucc = xs k

    fixedSnoc xs a k.castSucc = xs k when xs : Fin n → V and k : Fin n.

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.castAdd_to_castSucc {n m : ℕ} {k : Fin n} :
    Fin.castAdd (m + 1) k = (Fin.castAdd m k).castSucc

    Rewrite castAdd by using castAdd with one castSucc.

    source
    theorem FirstOrder.ZFC.FixedSnoc.coe_to_cast_add {n n' : ℕ} :
    Fin.ofNat (n + 1 + n') n = Fin.castAdd n' (Fin.last n)

    ofNat written by using Fin.last and castAdd.

    source
    theorem FirstOrder.ZFC.FixedSnoc.add_coe_eq_coe_add {n k m : ℕ} [NeZero (n + m)] :
    Fin.ofNat (n + m) n + Fin.ofNat (n + m) k = Fin.ofNat (n + m) (n + k)

    ofNat n + ofNat m = ofNat (n + m).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.sum_fixedSnoc_castSucc {V : Type u} {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {a : V} :
    (Sum.elim s (fixedSnoc xs a) ∘ Sum.map id fun (i : Fin n) => i.castSucc) = Sum.elim s xs

    Describes the cancellation of fixedSnoc and castSucc with Sum.elim.

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.fixedSnoc_castSucc {V : Type u} {n : ℕ} {xs : Fin n → V} {a : V} :
    fixedSnoc xs a ∘ Fin.castSucc = xs

    Describes the cancellation of fixedSnoc and castSucc with Sum.elim.

    source
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_1_0 {V : Type u} {a : V} :
    ![a] 0 = a

    ![a] 0 = a.

    source
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_2_0 {V : Type u} {a b : V} :
    ![a, b] 0 = a

    ![a, b] (0 : Fin 2) = a.

    source
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_1_0' {V : Type u} {a : V} :
    ![a] ↑0 = a

    ![a] 0 = a via Nat.cast.

    source
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_2_0' {V : Type u} {a b : V} :
    ![a, b] ↑0 = a

    ![a, b] 0 = a via Nat.cast.

    source
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_3_0' {V : Type u} {a b c : V} :
    ![a, b, c] ↑0 = a

    ![a, b, c] 0 = a via Nat.cast.

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_3_1' {V : Type u} {a b c : V} :
    ![a, b, c] ↑1 = b

    ![a, b, c] 1 = b via Nat.cast.

    source
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_3_2' {V : Type u} {a b c : V} :
    ![a, b, c] ↑2 = c

    ![a, b, c] 2 = c via Nat.cast.

    source
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_4_0' {V : Type u} {a b c d : V} :
    ![a, b, c, d] ↑0 = a

    ![a, b, c, d] 0 = a via Nat.cast.

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_4_1' {V : Type u} {a b c d : V} :
    ![a, b, c, d] ↑1 = b

    ![a, b, c, d] 1 = b via Nat.cast.

    source
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_4_2' {V : Type u} {a b c d : V} :
    ![a, b, c, d] ↑2 = c

    ![a, b, c, d] 2 = c via Nat.cast.

    source
    theorem FirstOrder.ZFC.FixedSnoc.Fintuple_4_3' {V : Type u} {a b c d : V} :
    ![a, b, c, d] ↑3 = d

    ![a, b, c, d] 3 = d via Nat.cast.

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_2_0 {V : Type u} {xs : Fin 0 → V} {a b : V} :
    fixedSnoc (fixedSnoc xs a) b 0 = a

    fixedSnoc (fixedSnoc xs a) b 0 = a over Fin 0.

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_2_1 {V : Type u} {xs : Fin 0 → V} {a b : V} :
    fixedSnoc (fixedSnoc xs a) b 1 = b

    fixedSnoc (fixedSnoc xs a) b 1 = b over Fin 0.

    source
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_0_2_0 {V : Type u} {xs : Fin 0 → V} {a b : V} :
    fixedSnoc (fixedSnoc xs a) b (OfNat.ofNat 0) = a

    fixedSnoc (fixedSnoc xs a) b 0 = a over Fin (0 + 2).

    source
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_0_2_1 {V : Type u} {xs : Fin 0 → V} {a b : V} :
    fixedSnoc (fixedSnoc xs a) b (OfNat.ofNat 1) = b

    fixedSnoc (fixedSnoc xs a) b 1 = b over Fin (0 + 2).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_0_3_0 {V : Type u} {xs : Fin 0 → V} {a b c : V} :
    fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c (OfNat.ofNat 0) = a

    fixedSnoc^3 ... 0 = a over Fin (0 + 3).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_0_3_1 {V : Type u} {xs : Fin 0 → V} {a b c : V} :
    fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c (OfNat.ofNat 1) = b

    fixedSnoc^3 ... 1 = b over Fin (0 + 3).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_0_3_2 {V : Type u} {xs : Fin 0 → V} {a b c : V} :
    fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c (OfNat.ofNat 2) = c

    fixedSnoc^3 ... 2 = c over Fin (0 + 3).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_0_4_0 {V : Type u} {xs : Fin 0 → V} {a b c d : V} :
    fixedSnoc (fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c) d (OfNat.ofNat 0) = a

    fixedSnoc^4 ... 0 = a over Fin (0 + 4).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_0_4_1 {V : Type u} {xs : Fin 0 → V} {a b c d : V} :
    fixedSnoc (fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c) d (OfNat.ofNat 1) = b

    fixedSnoc^4 ... 1 = b over Fin (0 + 4).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_0_4_2 {V : Type u} {xs : Fin 0 → V} {a b c d : V} :
    fixedSnoc (fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c) d (OfNat.ofNat 2) = c

    fixedSnoc^4 ... 2 = c over Fin (0 + 4).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_0_4_3 {V : Type u} {xs : Fin 0 → V} {a b c d : V} :
    fixedSnoc (fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c) d (OfNat.ofNat 3) = d

    fixedSnoc^4 ... 3 = d over Fin (0 + 4).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_n_2_0 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b : V} :
    fixedSnoc (fixedSnoc xs a) b ↑n = a

    fixedSnoc^2 ... n = a over Fin (n + 2).

    source
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_n_2_1 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b : V} :
    fixedSnoc (fixedSnoc xs a) b ↑(n + 1) = b

    fixedSnoc^2 ... (n+1) = b over Fin (n + 2).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_n_3_0 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b c : V} :
    fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c ↑n = a

    fixedSnoc^3 ... n = a over Fin (n + 3).

    source
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_n_3_1 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b c : V} :
    fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c ↑(n + 1) = b

    fixedSnoc^3 ... (n+1) = b over Fin (n + 3).

    source
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_n_3_2 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b c : V} :
    fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c ↑(n + 2) = c

    fixedSnoc^3 ... (n+2) = c over Fin (n + 3).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_n_4_0 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b c d : V} :
    fixedSnoc (fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c) d ↑n = a

    fixedSnoc^4 ... n = a over Fin (n + 4).

    source
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_n_4_1 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b c d : V} :
    fixedSnoc (fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c) d ↑(n + 1) = b

    fixedSnoc^4 ... (n+1) = b over Fin (n + 4).

    source
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_n_4_2 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b c d : V} :
    fixedSnoc (fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c) d ↑(n + 2) = c

    fixedSnoc^4 ... (n+2) = c over Fin (n + 4).

    source
    theorem FirstOrder.ZFC.FixedSnoc.FixedSnoc_n_4_3 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b c d : V} :
    fixedSnoc (fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c) d ↑(n + 3) = d

    fixedSnoc^4 ... (n+3) = d over Fin (n + 4).

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.fixedSnoc_castSucc_2 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b : V} :
    (fixedSnoc (fixedSnoc xs a) b ∘ fun (i : Fin n) => i.castSucc.castSucc) = xs

    fixedSnoc^2 ... ∘ castSucc^2 = xs.

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.fixedSnoc_castSucc_3 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b c : V} :
    (fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c ∘ fun (i : Fin n) => i.castSucc.castSucc.castSucc) = xs

    fixedSnoc^3 ... ∘ castSucc^3 = xs.

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.fixedSnoc_castSucc_4 {V : Type u} {n : ℕ} {xs : Fin n → V} {a b c d : V} :
    (fixedSnoc (fixedSnoc (fixedSnoc (fixedSnoc xs a) b) c) d ∘ fun (i : Fin n) => i.castSucc.castSucc.castSucc.castSucc) = xs

    fixedSnoc^4 ... ∘ castSucc^4 = xs.

    source
    @[simp]
    theorem FirstOrder.ZFC.FixedSnoc.fixedSnoc_castAdd_castSucc {V : Type u} {n n' : ℕ} {xs : Fin (n + n') → V} {x : V} :
    (fixedSnoc xs x ∘ fun (i : Fin n) => (Fin.castAdd n' i).castSucc) = xs ∘ fun (i : Fin n) => Fin.castAdd n' i

    fixedSnoc ∘ (castAdd ∘ castSucc) = xs ∘ castAdd.