English
Let f : α → β and s ⊆ α with a ∉ s. Then f is injective on insert a s if and only if f is injective on s and f(a) is not in the image f''s.
Русский
Пусть f : α → β и s ⊆ α, причём a ∉ s. Тогда f инъективна на вставке a в s тогда и только тогда, когда f инъективна на s и f(a) не принадлежит образу f[s].
LaTeX
$$$ \\operatorname{InjOn} f (\\operatorname{insert} a s) \\iff (\\operatorname{InjOn} f s \\land f a \\notin f'' s)$$$
Lean4
theorem injOn_insert {f : α → β} {s : Set α} {a : α} (has : a ∉ s) :
Set.InjOn f (insert a s) ↔ Set.InjOn f s ∧ f a ∉ f '' s :=
by
rw [← union_singleton, injOn_union (disjoint_singleton_right.2 has)]
simp
