keys_kreplace — Mathlib

English

The keys of kreplace do not depend on the replacement: (kreplace a b l).keys = l.keys.

Русский

Ключи у kreplace не зависят от замены: (kreplace a b l).keys = l.keys.

LaTeX

$$$ (\mathrm{kreplace}(a,b,l)).keys = l.keys $$$

Lean4

theorem keys_kreplace (a : α) (b : β a) : ∀ l : List (Sigma β), (kreplace a b l).keys = l.keys :=
  lookmap_map_eq _ _ <| by
    rintro ⟨a₁, b₂⟩ ⟨a₂, b₂⟩
    dsimp
    split_ifs with h <;> simp +contextual [h]

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