English
If f is injective and s does not contain a fixed element of the nonempty type, then preimage of s under invFun f equals image f s.
Русский
Если f инъективна и заданное элемент не принадлежит s, то прообраз invFun f по s равен image f s.
LaTeX
$$$[n: Nonempty\\alpha] \\{f:\\alpha\\to\\beta\\} \\rightarrow Injective f \\\\rightarrow \\forall s, s \\notin (Classical.choice n) \\Rightarrow preimage (invFun f) s = image f s$$$
Lean4
theorem preimage_invFun_of_notMem [n : Nonempty α] {f : α → β} (hf : Injective f) {s : Set α}
(h : Classical.choice n ∉ s) : invFun f ⁻¹' s = f '' s :=
by
ext x
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
· rw [mem_preimage, leftInverse_invFun hf, hf.mem_set_image]
· have : x ∉ f '' s := fun h' => hx (image_subset_range _ _ h')
simp only [mem_preimage, invFun_neg hx, h, this]
