kreplace_nodupKeys — Mathlib

English

Kreplace preserves the NodupKeys property up to equivalence: (kreplace a b l).NodupKeys ↔ l.NodupKeys.

Русский

Kreplace сохраняет свойство NodupKeys вплоть до эквивалентности: (kreplace a b l).NodupKeys ↔ l.NodupKeys.

LaTeX

$$$ \mathrm{kreplace}(a,b,l).NodupKeys \iff l.NodupKeys $$$

Lean4

theorem kreplace_nodupKeys (a : α) (b : β a) {l : List (Sigma β)} : (kreplace a b l).NodupKeys ↔ l.NodupKeys := by
  simp [NodupKeys, keys_kreplace]

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