image_surjective — Mathlib

English

If f is surjective, the image map is surjective: for every S ⊆ β there exists T ⊆ α with f''T = S.

Русский

Если f сюръективно, отображение образа является сюръективным: для каждого подмножества S ⊆ β существует подмножество T ⊆ α такое, что f''T = S.

LaTeX

$$$\forall S \subseteq \beta,\; \exists T \subseteq \alpha:\ f''T = S.$$$

Lean4

theorem image_surjective (hf : Surjective f) : Surjective (image f) :=
  by
  intro s
  use f ⁻¹' s
  rw [hf.image_preimage]

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