keys — Mathlib

English

The set of keys of a Finmap is the Finset consisting of all first elements appearing in its entries.

Русский

Множество ключей Finmap состоит из первых компонентов всех пар в записях.

LaTeX

$$$$ \mathrm{keys}(s) = \langle s.\mathrm{entries}.\mathrm{keys}, \; s.\mathrm{nodupKeys}.\mathrm{nodup\_keys} \rangle $$$$

Lean4

/-- The set of keys of a finite map. -/
def keys (s : Finmap β) : Finset α :=
  ⟨s.entries.keys, s.nodupKeys.nodup_keys⟩

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