theorem LentilLib.forall_unit {p : PUnit → Prop} : (∀ (x : PUnit), p x) ↔ p PUnit.unit

theorem LentilLib.exists_unit {p : PUnit → Prop} : (∃ (x : PUnit), p x) ↔ p PUnit.unit

theorem LentilLib.List.mem_forall_iff_fin_index {α : Type u} (l : List α) (p : α → Prop) : (∀ (x : α), x ∈ l → p x) ↔ ∀ (x : Fin l.length), p l[x]

theorem LentilLib.List.mem_exists_iff_fin_index {α : Type u} (l : List α) (p : α → Prop) : (∃ (x : α), x ∈ l ∧ p x) ↔ ∃ (x : Fin l.length), p l[x]

theorem LentilLib.List.finRange_fin_in (n : Nat) (x : Fin n) : x ∈ List.finRange n

theorem LentilLib.List.take_getElem_drop {α : Type u} {l : List α} {n : Nat} (h : n < l.length) : List.take n l ++ l[n] :: List.drop (n + 1) l = l

theorem LentilLib.List.modify_perm {α : Type u} {l : List α} {idx : Nat} (h : idx < l.length) (f : α → α) : (l ++ [f l[idx]]).Perm (l.modify idx f ++ [l[idx]])

theorem LentilLib.List.findFindIdx {α : Type u} {l : List α} {p : α → Bool} {res : α} (hpred : List.find? p l = some res) : p res = true ∧ ∃ (idx : Nat), ∃ (hidx : idx < l.length), l[idx] = res ∧ List.findIdx? p l = some idx

def LentilLib.List.foldrD {β : Type v} (f : β → β → β) (d : β) : List β → β

Right-fold a non-empty list, returning the default d on the empty list.

Equations

• LentilLib.List.foldrD f d [a] = a
• LentilLib.List.foldrD f d (a :: as) = f a (LentilLib.List.foldrD f d as)
• LentilLib.List.foldrD f d [] = d

theorem LentilLib.List.foldrD_eq_foldr {β : Type v} (f : β → β → β) (d : β) (l : List β) (h : ∀ (x : β), f x d = x) : foldrD f d l = List.foldr f d l

def LentilLib.List.containsDuplicateElemHashable {α : Type u} [BEq α] [Hashable α] (l : List α) : Bool

Whether a list contains a duplicate element, using hashing.

Equations

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

theorem LentilLib.Nat.find_min {p : Nat → Prop} (n : Nat) (h : p n) : ∃ (n' : Nat), n' ≤ n ∧ p n' ∧ ∀ (m : Nat), m < n' → ¬p m

theorem LentilLib.Nat.find_min' {p : Nat → Prop} (n : Nat) (h : p n) : ∃ (n' : Nat), n' ≤ n ∧ p n' ∧ ∀ (m : Nat), p m → n' ≤ m