Constructions of embeddings of Fin n into a type

• Fin.Embedding.cons : from an embedding x : Fin n ↪ α and a : α such that a ∉ x.range, construct an embedding Fin (n + 1) ↪ α by putting a at 0

• Fin.Embedding.tail: the tail of an embedding x : Fin (n + 1) ↪ α

• Fin.Embedding.snoc : from an embedding x : Fin n ↪ α and a : α such that a ∉ x.range, construct an embedding Fin (n + 1) ↪ α by putting a at the end.

• Fin.Embedding.init: the init of an embedding x : Fin (n + 1) ↪ α

• Fin.Embedding.append : merges two embeddings Fin m ↪ α and Fin n ↪ α into an embedding Fin (m + n) ↪ α if they have disjoint ranges

def Fin.Embedding.tail {α : Type u_1} {n : ℕ} (x : Fin (n + 1) ↪ α) : Fin n ↪ α

Remove the first element from an injective (n + 1)-tuple.

Equations

• Fin.Embedding.tail x = { toFun := Fin.tail ⇑x, inj' := ⋯ }

@[simp]

theorem Fin.Embedding.coe_tail {α : Type u_1} {n : ℕ} (x : Fin (n + 1) ↪ α) : ⇑(tail x) = Fin.tail ⇑x

def Fin.Embedding.cons {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : ¬a ∈ Set.range ⇑x) : Fin (n + 1) ↪ α

Adding a new element at the beginning of an injective n-tuple, to get an injective n+1-tuple.

Equations

• Fin.Embedding.cons x ha = { toFun := Fin.cons a ⇑x, inj' := ⋯ }

@[simp]

theorem Fin.Embedding.coe_cons {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : ¬a ∈ Set.range ⇑x) : ⇑(cons x ha) = Fin.cons a ⇑x

theorem Fin.Embedding.tail_cons {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : ¬a ∈ Set.range ⇑x) : tail (cons x ha) = x

def Fin.Embedding.init {α : Type u_1} {n : ℕ} (x : Fin (n + 1) ↪ α) : Fin n ↪ α

Remove the last element from an injective (n + 1)-tuple.

Equations

• Fin.Embedding.init x = { toFun := Fin.init ⇑x, inj' := ⋯ }

def Fin.Embedding.snoc {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : ¬a ∈ Set.range ⇑x) : Fin (n + 1) ↪ α

Adding a new element at the end of an injective n-tuple, to get an injective n+1-tuple.

Equations

• Fin.Embedding.snoc x ha = { toFun := Fin.snoc (⇑x) a, inj' := ⋯ }

@[simp]

theorem Fin.Embedding.coe_snoc {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : ¬a ∈ Set.range ⇑x) : ⇑(snoc x ha) = Fin.snoc (⇑x) a

theorem Fin.Embedding.init_snoc {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : ¬a ∈ Set.range ⇑x) : init (snoc x ha) = x

theorem Fin.Embedding.snoc_castSucc {α : Type u_1} {n : ℕ} {x : Fin n ↪ α} {a : α} {ha : ¬a ∈ Set.range ⇑x} {i : Fin n} : (snoc x ha) i.castSucc = x i

theorem Fin.Embedding.snoc_last {α : Type u_1} {n : ℕ} {x : Fin n ↪ α} {a : α} {ha : ¬a ∈ Set.range ⇑x} : (snoc x ha) (last n) = a

def Fin.Embedding.append {α : Type u_1} {m n : ℕ} {x : Fin m ↪ α} {y : Fin n ↪ α} (h : Disjoint (Set.range ⇑x) (Set.range ⇑y)) : Fin (m + n) ↪ α

Append a Fin n ↪ α at the end of a Fin m ↪ α if their ranges are disjoint.

Equations

• Fin.Embedding.append h = { toFun := Fin.append ⇑x ⇑y, inj' := ⋯ }

@[simp]

theorem Fin.Embedding.coe_append {α : Type u_1} {m n : ℕ} {x : Fin m ↪ α} {y : Fin n ↪ α} (h : Disjoint (Set.range ⇑x) (Set.range ⇑y)) : ⇑(append h) = Fin.append ⇑x ⇑y

def Function.Embedding.twoEmbeddingEquiv {α : Type u_1} : (Fin 2 ↪ α) ≃ ↑{(a, b) : α × α | a ≠ b}

The natural equivalence of Fin 2 ↪ α with pairs (a, b) of distinct elements of α.

Equations

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

def Function.Embedding.embFinTwo {α : Type u_1} {a b : α} (h : a ≠ b) : Fin 2 ↪ α

Two distinct elements of α give an embedding Fin 2 ↪ α.

Equations

• Function.Embedding.embFinTwo h = Function.Embedding.twoEmbeddingEquiv.invFun ⟨(a, b), h⟩

theorem Function.Embedding.embFinTwo_apply_zero {α : Type u_1} {a b : α} (h : a ≠ b) : (embFinTwo h) 0 = a

theorem Function.Embedding.embFinTwo_apply_one {α : Type u_1} {a b : α} (h : a ≠ b) : (embFinTwo h) 1 = b