English
Let f be injective. For any subset s, the complement of the image f''s equals the union of the image of the complement s^c with the complement of the range of f.
Русский
Пусть f инъективна. Для любого множества s выполнено: дополнение образа f''s равно объединению образа дополнения s с дополнением образа f.
LaTeX
$$$ (f''s)^c = f''(s^c) \cup (\mathrm{range}(f))^c $$$
Lean4
theorem compl_image_eq (hf : Injective f) (s : Set α) : (f '' s)ᶜ = f '' sᶜ ∪ (range f)ᶜ :=
by
ext y
rcases em (y ∈ range f) with (⟨x, rfl⟩ | hx)
· simp [hf.eq_iff]
· grind