range_specComap_of_surjective — Mathlib

English

If f is surjective, then the range of f.specComap equals the zero locus of ker f.

Русский

Если f сюръективно, то диапазон f.specComap равен нулевой локусеker f.

LaTeX

$$$\\operatorname{range} f.{\\rm specComap} = \\operatorname{zeroLocus}(\\ker f)$$$

Lean4

theorem range_specComap_of_surjective (hf : Surjective f) : Set.range f.specComap = zeroLocus (ker f) :=
  by
  rw [← Set.image_univ]
  convert image_specComap_zeroLocus_eq_zeroLocus_comap _ _ hf _
  rw [zeroLocus_bot]

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