keys_cons — Mathlib

English

The operation of prepending a key to a multiset of dependent pairs corresponds to prepending its key to the keys multiset: keys(⟨a,b⟩ ::ₘ s) = a ::ₘ keys s.

Русский

Операция добавления пары на перед Multiset зависимых элементов соответствует добавлению ключа a в множество ключей: keys(⟨a,b⟩ ::ₘ s) = a ::ₘ keys s.

LaTeX

$$$$ \operatorname{keys}(\langle a,b\rangle ::_m s) = a ::_m \operatorname{keys}(s) $$$$

Lean4

@[simp]
theorem keys_cons {a : α} {b : β a} {s : Multiset (Sigma β)} : keys (⟨a, b⟩ ::ₘ s) = a ::ₘ keys s := by simp [keys]

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