English
For a function b : α → β and a fixed k ∈ β, the image of the subtype { a ∈ α | b(a) ≠ k } under b equals the image of b on univ with k erased: im(b|_{b(a)≠k}) = im(b) \ {k}.
Русский
Для функции b : α → β и фиксированного k ∈ β образ подтипа { a ∈ α | b(a) ≠ k } равен образу функции b на всём множестве с вычитанием значения k: im(b|_{b(a)≠k}) = im(b) \\ {k}.
LaTeX
$$$$\\operatorname{image}(\\lambda i : \\{ a \\mid b a \\neq k \\}, b(i)) \\,\\operatorname{univ} = (\\operatorname{image} b \\operatorname{univ}) \\setminus \\{k\\}.$$$$
Lean4
theorem image_subtype_ne_univ_eq_image_erase [Fintype α] [DecidableEq β] (k : β) (b : α → β) :
image (fun i : { a // b a ≠ k } => b ↑i) univ = (image b univ).erase k :=
by
apply subset_antisymm
· rw [image_subset_iff]
intro i _
apply mem_erase_of_ne_of_mem i.2 (mem_image_of_mem _ (mem_univ _))
· intro i hi
rw [mem_image]
rcases mem_image.1 (erase_subset _ _ hi) with ⟨a, _, ha⟩
subst ha
exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩
