nodupKeys_cons — Mathlib

English

For a head element s and a tail l, NodupKeys (s :: l) holds iff s.1 is not in l.keys and NodupKeys l holds.

Русский

Для головы s и хвоста l выполняется: NodupKeys (s :: l) эквивалентно (s.1 ∉ l.keys) и NodupKeys l.

LaTeX

$$$ \\mathrm{NodupKeys}(s :: l) \\iff \\bigl(s.1 \\notin l.keys\\bigr) \\land \\mathrm{NodupKeys}(l) $$$

Lean4

@[simp]
theorem nodupKeys_cons {s : Sigma β} {l : List (Sigma β)} : NodupKeys (s :: l) ↔ s.1 ∉ l.keys ∧ NodupKeys l := by
  simp [keys, NodupKeys]

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