image_compl_eq_range_diff_image — Mathlib

English

For an injective f, the image of the complement equals the range minus the image of the set: f'' sᶜ = range f \\ f'' s.

Русский

При инъективной f образ дополнения множества равен диапазону минус образ множества: f'' sᶜ = range f \\ f'' s.

LaTeX

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

Lean4

theorem image_compl_eq_range_diff_image {f : α → β} (hf : Injective f) (s : Set α) : f '' sᶜ = range f \ f '' s := by
  rw [← image_univ, ← image_diff hf, compl_eq_univ_diff]

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