English
If f is injective and a is in the domain choice, then the preimage of a subset s under invFun f is the union of the image of s and the complement of range f.
Русский
Если f инъективна и a принадлежит выбранному элементу, то прообраз invFun f по s равен image f s ∪ (range f)ᶜ.
LaTeX
$$$[n: Nonempty\\alpha] \\{f:\\alpha\\to\\beta\\} \\to \\forall s, invFun f \\;^{-1}(s) = f '' s \\cup (range f)^c$$$
Lean4
theorem preimage_invFun_of_mem [n : Nonempty α] {f : α → β} (hf : Injective f) {s : Set α}
(h : Classical.choice n ∈ s) : invFun f ⁻¹' s = f '' s ∪ (range f)ᶜ :=
by
ext x
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
·
simp only [mem_preimage, mem_union, mem_compl_iff, mem_range_self, not_true, or_false, leftInverse_invFun hf _,
hf.mem_set_image]
· simp only [mem_preimage, invFun_neg hx, h, hx, mem_union, mem_compl_iff, not_false_iff, or_true]
