exists_eq_graphOn — Mathlib

English

There exists a representation of a relation s as a graph of a function f with some t, provided Nonempty β.

Русский

Существует представление отношения s как графа функции f на некотором t при условии непустости β.

LaTeX

$$$(\\exists f : α \\to β)(\\exists t : Set α)(s = \\mathrm{graphOn} f t) \\iff \\mathrm{InjOn}(\\mathrm{Prod.fst}, s)\\;[\\text{при } [Nonempty \\beta]]$$$

Lean4

theorem exists_eq_graphOn [Nonempty β] {s : Set (α × β)} : (∃ f t, s = graphOn f t) ↔ InjOn Prod.fst s :=
  .trans ⟨fun ⟨f, t, hs⟩ ↦ ⟨f, by rw [hs, image_fst_graphOn]⟩, fun ⟨f, hf⟩ ↦ ⟨f, _, hf⟩⟩ exists_eq_graphOn_image_fst

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