compl_range_subset_kernImage — Mathlib

English

The complement of the range is contained in kernImage f s for every s: (range f)^c ⊆ kernImage f s.

Русский

Дополнение диапазона содержится в kernImage f s для любого s: (range f)^c ⊆ kernImage f s.

LaTeX

$${\$range f\$}^c \\subseteq \\mathrm{kernImage}\\, f\\, s$$

Lean4

theorem compl_range_subset_kernImage {s : Set α} : (range f)ᶜ ⊆ kernImage f s :=
  by
  rw [← kernImage_empty]
  exact kernImage_mono (empty_subset _)

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