mem_insert — Mathlib

English

Let S be an AList β. For any a, a' and any b' : β a', the membership of an element with key a in the inserted structure insert a' b' S is equivalent to a = a' or a appears in S.

Русский

Пусть S является AList β. Для любых a, a' и b' : β a' членство элемента с ключом a в вставке insert a' b' S эквивалентно либо a = a', либо a встречается в S.

LaTeX

$$$ a \in \mathrm{insert}(a', b', s) \iff a = a' \lor a \in s $$$

Lean4

@[simp]
theorem mem_insert {a a'} {b' : β a'} (s : AList β) : a ∈ insert a' b' s ↔ a = a' ∨ a ∈ s :=
  mem_keys_kinsert

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