insert_singleton_eq — Mathlib

English

Inserting b into a singleton at a yields the same singleton with b as the value: insert a b (singleton a b') = singleton a b.

Русский

Вставка значения b в одиночное отображение на a дает одиночное отображение с b: insert a b (singleton a b') = singleton a b.

LaTeX

$$$ \text{insert}\ a\ b\ (\text{singleton } a\ b') = \text{singleton } a\ b $$$

Lean4

@[simp]
theorem insert_singleton_eq {a : α} {b b' : β a} : insert a b (singleton a b') = singleton a b := by
  simp only [singleton, Finmap.insert_toFinmap, AList.insert_singleton_eq]

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