range_diff_image — Mathlib

English

The range minus the image of s equals the image of the complement of s, for injective f: range f \\ f '' s = f '' sᶜ.

Русский

Диапазон минус образ s равен образу дополнения s: range f \\ f '' s = f '' sᶜ.

LaTeX

$$$ \\operatorname{range} f \\setminus f'' s = f'' s^{\\complement}$$$

Lean4

/-- Alias of `Set.image_compl_eq_range_sdiff_image`. -/
theorem range_diff_image {f : α → β} (hf : Injective f) (s : Set α) : range f \ f '' s = f '' sᶜ := by
  rw [image_compl_eq_range_diff_image hf]

Похожие утверждения