English
There exists a function f: α → β such that f a = b for given a ∈ α and b ∈ β; in particular, the constant function f(x) = b witnesses existence.
Русский
Существует функция f: α → β такая, что f(a) = b для заданных a ∈ α и b ∈ β; константная функция f(x) = b служит свидетелем существования.
LaTeX
$$$$\\exists f:\\, \\alpha \\to \\beta,\\; f(a)=b.$$$$
Lean4
/-- The constant function witnesses that
there exists a function sending a given term to a given term.
This is sometimes useful in `simp` to discharge side conditions.
-/
theorem exists_apply_eq (a : α) (b : β) : ∃ f : α → β, f a = b :=
⟨fun _ ↦ b, rfl⟩
