sublist_dlookup — Mathlib

English

If l₁ is a sublist of l₂, then any element b in the dlookup a of l₁ is also in the dlookup a of l₂ (for all a).

Русский

Если l₁ является подсписком l₂, то любой элемент b из dlookup a l₁ принадлежит dlookup a l₂.

LaTeX

$$$ \text{l₁.Sublist l₂} \; \rightarrow\; \forall a, b, \, b \in dlookup a\ l₁ \rightarrow b \in dlookup a\ l₂ $$$

Lean4

theorem sublist_dlookup {l₁ l₂ : List (Sigma β)} {a : α} {b : β a} (nd₂ : l₂.NodupKeys) (s : l₁ <+ l₂)
    (mem : b ∈ l₁.dlookup a) : b ∈ l₂.dlookup a := by
  grind [Option.mem_def, => perm_dlookup, → Sublist.exists_perm_append]

Похожие утверждения