compl_image_eq — Mathlib

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

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