insert_of_notMem — Mathlib

English

If a ∉ s, then insert a b s equals the AList whose entries start with ⟨a,b⟩ and then s.entries.

Русский

Если a ∉ s, то insert a b s равно AList с записями, начинающимися с ⟨a,b⟩, затем s.entries.

LaTeX

$$a \notin s \Rightarrow insert(a,b,s) = ⟨⟨a,b⟩ :: s.entries, nodupKeys_cons.2 ⟨a∉s, s.2⟩⟩$$

Lean4

theorem insert_of_notMem {a} {b : β a} {s : AList β} (h : a ∉ s) :
    insert a b s = ⟨⟨a, b⟩ :: s.entries, nodupKeys_cons.2 ⟨h, s.2⟩⟩ :=
  ext <| entries_insert_of_notMem h

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