Mathlib.NumberTheory.LSeries.Convergence._auxLemma.2

theorem Mathlib.NumberTheory.LSeries.Convergence._auxLemma.2 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (y : β), (y ∈ f '' s) = ∃ x ∈ s, f x = y

The theorem, `Mathlib.NumberTheory.LSeries.Convergence._auxLemma.2`, states that for any types `α` and `β`, a function `f` from `α` to `β`, a set `s` of type `α`, and an element `y` of type `β`, the condition "y is in the image of the set s under the function f" is equivalent to the existence of an element x in the set s such that f applied to x equals y. This theorem essentially establishes the definition of the image of a set under a function in the context of Lean 4.

More concisely: For any types `α`, `β`, function `f` from `α` to `β`, set `s` of type `α`, and element `y` of type `β`, the condition `y ∈ im f s` is equivalent to the existence of `x ∈ s` such that `f x = y`.