English
There exists f and t such that s = graphOn f t if and only if Prod.fst is injective on s.
Русский
Существуют функции f и множества t such that s = graphOn f t тогда и только тогда, когда Prod.fst инъективна на s.
LaTeX
$$$(\\exists f, t)(s = \\mathrm{graphOn} f t) \\iff \\mathrm{InjOn}(\\mathrm{Prod.fst}, s).$$$
Lean4
theorem exists_eq_graphOn_image_fst [Nonempty β] {s : Set (α × β)} :
(∃ f : α → β, s = graphOn f (Prod.fst '' s)) ↔ InjOn Prod.fst s :=
by
refine ⟨?_, fun h ↦ ?_⟩
· rintro ⟨f, hf⟩
rw [hf]
exact InjOn.image_of_comp <| injOn_id _
· have : ∀ x ∈ Prod.fst '' s, ∃ y, (x, y) ∈ s := forall_mem_image.2 fun (x, y) h ↦ ⟨y, h⟩
choose! f hf using this
rw [forall_mem_image] at hf
use f
rw [graphOn, image_image, EqOn.image_eq_self]
exact fun x hx ↦ h (hf hx) hx rfl
