theorem Nat.zero_lt_of_not_zero {n : ℕ} (hn : n ≠ 0) : 0 < n

def List.finIdxOf {α : Type u_1} {x : α} [DecidableEq α] (l : List α) (hx : x ∈ l) : Fin l.length

Equations

• l.finIdxOf hx = ⟨List.idxOf x l, ⋯⟩

@[simp]

theorem List.get_finIdxOf {α : Type u_1} {l : List α} {x : α} [DecidableEq α] {hx : x ∈ l} : l.get (l.finIdxOf hx) = x

theorem List.neq_findIdxOf_of_neq {α : Type u_1} {l : List α} {x y : α} [DecidableEq α] {hx : x ∈ l} {hy : y ∈ l} (exy : x ≠ y) : l.finIdxOf hx ≠ l.finIdxOf hy

theorem List.range.le_chain'_succ {n : ℕ} : Chain' (fun (x1 x2 : ℕ) => x1 < x2) (range (n + 1))

@[simp]

theorem List.range.le_chain' {n : ℕ} : Chain' (fun (x1 x2 : ℕ) => x1 < x2) (range n)

theorem List.finRange.le_chain'_succ {n : ℕ} : Chain' (fun (x1 x2 : Fin (n + 1)) => x1 < x2) (finRange (n + 1))

@[simp]

theorem List.finRange.le_chain' {n : ℕ} : Chain' (fun (x1 x2 : Fin n) => x1 < x2) (finRange n)

theorem List.Chain'.of_lt {α : Type u_1} {R : α → α → Prop} [IsTrans α R] {l : List α} {i j : Fin l.length} (h : Chain' R l) (hij : i < j) : R (l.get i) (l.get j)

theorem List.Chain'.connected_of_trans' {α : Type u_1} {R : α → α → Prop} [IsTrans α R] {l : List α} {i j : Fin l.length} (h : Chain' R l) (eij : i ≠ j) : R (l.get i) (l.get j) ∨ R (l.get j) (l.get i)

theorem List.Chain'.connected_of_trans {α : Type u_1} {x y : α} {R : α → α → Prop} [IsTrans α R] {l : List α} [DecidableEq α] (h : Chain' R l) (hx : x ∈ l) (hy : y ∈ l) (exy : x ≠ y) : R x y ∨ R y x

theorem List.Chain'.noDup_of_irrefl_trans {α : Type u_1} {R : α → α → Prop} [IsTrans α R] {l : List α} (h : Chain' R l) [IsIrrefl α R] : l.Nodup

theorem List.mem_head?_eq_head {α : Type u_1} {l : List α} {a : α} : a ∈ l.head? → ∃ (h : l ≠ []), a = l.head h

theorem List.concat_head?_eq_head {α : Type u_1} {l : List α} {a : α} (lh : l ≠ []) : (l.concat a).head? = some (l.head lh)

theorem List.chain'_concat {α : Type u_1} {l : List α} {R : α → α → Prop} {a : α} : Chain' R (l.concat a) ↔ Chain' R l ∧ ∀ x ∈ l.getLast?, R x a

theorem List.chain'_concat_of_not_nil {α : Type u_1} {l : List α} {R : α → α → Prop} {a : α} (hl : l ≠ []) : Chain' R (l.concat a) ↔ Chain' R l ∧ R (l.getLast hl) a

theorem List.rel_head_of_chain'_trans {α : Type u_1} {l : List α} [DecidableEq α] {R : α → α → Prop} [IsTrans α R] (h : Chain' R l) (lh : l ≠ []) (x : α) : x ∈ l → x ≠ l.head lh → R (l.head lh) x

theorem List.rel_head_of_chain'_preorder {α : Type u_1} {l : List α} [DecidableEq α] {R : α → α → Prop} [IsPreorder α R] (h : Chain' R l) (lh : l ≠ []) (x : α) : x ∈ l → R (l.head lh) x

theorem List.rel_getLast_of_chain'_trans {α : Type u_1} {l : List α} [DecidableEq α] {R : α → α → Prop} [IsTrans α R] (h : Chain' R l) (lh : l ≠ []) (x : α) : x ∈ l → x ≠ l.getLast lh → R x (l.getLast lh)

theorem List.rel_getLast_of_chain'_preorder {α : Type u_1} {l : List α} [DecidableEq α] {R : α → α → Prop} [IsPreorder α R] (h : Chain' R l) (lh : l ≠ []) (x : α) : x ∈ l → R x (l.getLast lh)

def List.embedding_of_exists_noDup {α : Type u_1} {n : ℕ} {l : List α} (hl₁ : l.Nodup) (hl₂ : l.length = n) : Fin n ↪ α

Equations

• List.embedding_of_exists_noDup hl₁ hl₂ = { toFun := fun (x : Fin n) => match x with | ⟨i, hi⟩ => l.get ⟨i, ⋯⟩, inj' := ⋯ }