Documentation

Std.Data.DHashMap.Internal.List.Sublist

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.Sublist

source
inductive Std.DHashMap.Internal.List.Sublist {α : Type u} :
List α → List α → Prop

Internal implementation detail of the hash map

Instances For
    source
    @[simp]
    theorem Std.DHashMap.Internal.List.sublist_nil {α : Type u} {l : List α} :
    Std.DHashMap.Internal.List.Sublist [] l
    source
    theorem Std.DHashMap.Internal.List.Sublist.length_le {α : Type u} {l₁ : List α} {l₂ : List α} (h : Std.DHashMap.Internal.List.Sublist l₁ l₂) :
    l₁.length ≤ l₂.length
    source
    theorem Std.DHashMap.Internal.List.Sublist.of_cons_left {α : Type u} {l₁ : List α} {l₂ : List α} {a : α} (h : Std.DHashMap.Internal.List.Sublist (a :: l₁) l₂) :
    Std.DHashMap.Internal.List.Sublist l₁ l₂
    source
    @[simp]
    theorem Std.DHashMap.Internal.List.Sublist.cons_iff {α : Type u} {a : α} {l₁ : List α} {l₂ : List α} :
    Std.DHashMap.Internal.List.Sublist (a :: l₁) (a :: l₂) ↔ Std.DHashMap.Internal.List.Sublist l₁ l₂
    source
    theorem Std.DHashMap.Internal.List.Sublist.map {α : Type u} {β : Type v} (f : α → β) {l₁ : List α} {l₂ : List α} (h : Std.DHashMap.Internal.List.Sublist l₁ l₂) :
    Std.DHashMap.Internal.List.Sublist (List.map f l₁) (List.map f l₂)
    source
    theorem Std.DHashMap.Internal.List.Sublist.mem {α : Type u} {l₁ : List α} {l₂ : List α} (h : Std.DHashMap.Internal.List.Sublist l₁ l₂) {a : α} :
    a ∈ l₁ → a ∈ l₂
    source
    theorem Std.DHashMap.Internal.List.erase_sublist {α : Type u} [BEq α] (l : List α) (a : α) :
    Std.DHashMap.Internal.List.Sublist (l.erase a) l
    source
    theorem Std.DHashMap.Internal.List.filter_sublist {α : Type u} (l : List α) {f : α → Bool} :
    Std.DHashMap.Internal.List.Sublist (List.filter f l) l