update_injective — Mathlib

English

For any fixed a' and a family f, the map v ↦ update f a' v is injective; i.e., if update f a' v1 = update f a' v2 then v1 = v2.

Русский

Для фиксированной точки a' и семейства функций инъективность отображения обновления: если обновление равно обновлению, то значения совпадают.

LaTeX

$$$\\text{Injective}(\\lambda v:\\beta a' ,\\ update\\ f\\ a'\\ v)$$$

Lean4

theorem update_injective (f : ∀ a, β a) (a' : α) : Injective (update f a') := fun v v' h ↦
  by
  have := congr_fun h a'
  rwa [update_self, update_self] at this

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