This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.
File contents: tiny private implementation of List.Pairwise
@[simp]
theorem
Std.DHashMap.Internal.List.Pairwise.perm
{α : Type u}
{P : α → α → Prop}
(hP : ∀ {x y : α}, P x y → P y x)
{l : List α}
{l' : List α}
(h : l.Perm l')
:
theorem
Std.DHashMap.Internal.List.Pairwise.sublist
{α : Type u}
{P : α → α → Prop}
{l : List α}
{l' : List α}
(h : Std.DHashMap.Internal.List.Sublist l l')
:
theorem
Std.DHashMap.Internal.List.pairwise_cons
{α : Type u}
{P : α → α → Prop}
{a : α}
{l : List α}
:
Std.DHashMap.Internal.List.Pairwise P (a :: l) ↔ (∀ (y : α), y ∈ l → P a y) ∧ Std.DHashMap.Internal.List.Pairwise P l