replace_toFinmap — Mathlib

English

Replacing the value at a single key a with b in a Finmap s does not change membership of any key a'.

Русский

Замена значения для ключа a на b в отображении Finmap s не изменяет членство любого ключа a'.

LaTeX

$$$ a' \in replace\ a\ b\ s \iff a' \in s. $$$

Lean4

@[simp]
theorem replace_toFinmap (a : α) (b : β a) (s : AList β) : replace a b ⟦s⟧ = (⟦s.replace a b⟧ : Finmap β) := by
  simp [replace]

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