image_surjective — Mathlib

English

For sets and a function f, the surjectivity of the image map on sets is equivalent to the surjectivity of f itself.

Русский

Для отображения f: α → β сопоставление образов подмножеств по f расталкивает сюръективность отображения образов множеств и саму сюръективность f.

LaTeX

$$$\operatorname{Surjective}(\operatorname{image} f) \iff \operatorname{Surjective} f$$$

Lean4

@[simp]
theorem image_surjective : Surjective (image f) ↔ Surjective f :=
  by
  refine ⟨fun h y => ?_, Surjective.image_surjective⟩
  rcases h { y } with ⟨s, hs⟩
  have := mem_singleton y; rw [← hs] at this; rcases this with ⟨x, _, hx⟩
  exact ⟨x, hx⟩

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