lean_workbook_plus_59850
ProvedWe say that from is surjective if
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59850 {f : ℕ → ℕ} : (∀ b, ∃ a, f a = b) ↔ Set.range f = Set.univ := by sorrySource
We say that from is surjective if
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_59850 {f : ℕ → ℕ} : (∀ b, ∃ a, f a = b) ↔ Set.range f = Set.univ := by sorry