The kernel of a one-point identification

Updating the identity at b to a identifies just those two points. No distinctness, finiteness or injectivity premise is required. This elementary original identity supports comparison of actual source labels with their dense incidence names.

theorem Function.update_id_apply_eq_iff {α : Sort u_1} [DecidableEq α] (a b x y : α) : update id b a x = update id b a y ↔ x = y ∨ x = a ∧ y = b ∨ x = b ∧ y = a

A one-point update of the identity equates precisely equal points or the selected pair.