subset_range_of_surjective — Mathlib

English

If f is surjective, then every subset s of the codomain is contained in the range of f.

Русский

Если f сюръективна, то любая подмножество s кодомона содержится в образе f.

LaTeX

$$$ \\text{Surjective}(f) \\Rightarrow \\forall s,\\; s \\subseteq \\operatorname{range} f.$$$

Lean4

@[simp]
theorem subset_range_of_surjective {f : α → β} (h : Surjective f) (s : Set β) : s ⊆ range f :=
  Surjective.range_eq h ▸ subset_univ s

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