setValue_eq_iff — Mathlib

English

For f: α ↪ β and a,a',b, the equation (f.setValue a b) a' = b holds if and only if a' = a.

Русский

Для f: α ↪ β, a,a' и b:β выполняется (f.setValue a b) a' = b ↔ a' = a.

LaTeX

$$$(f.setValue\\ a\\ b)\\ a' = b \\iff a' = a$$$

Lean4

@[simp]
theorem setValue_eq_iff {α β} (f : α ↪ β) {a a' : α} {b : β} [∀ a', Decidable (a' = a)] [∀ a', Decidable (f a' = b)] :
    setValue f a b a' = b ↔ a' = a :=
  (setValue f a b).injective.eq_iff' <| setValue_eq ..

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