mem_keys_kinsert — Mathlib

English

A key membership fact: an element a belongs to the keys of kinsert a' b' l precisely when a = a' or a belongs to the keys of l.

Русский

Члены ключей kinsert a' b' l удовлетворяют: a принадлежит ключам kinsert a' b' l тогда, когда a = a' или a принадлежит ключам l.

LaTeX

$$$a \\in (kinsert a' b' l).keys \\iff a = a' \\lor a \\in l.keys$$$

Lean4

theorem mem_keys_kinsert {a a'} {b' : β a'} {l : List (Sigma β)} : a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys :=
  by by_cases h : a = a' <;> simp [h]

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