graphFunctor_map — Mathlib

English

Let X and Y be types and f: X → Y. The graph of f relates an element x in X to an element y in Y exactly when y = f(x). In other words, the graph relation of f consists precisely of all pairs (x, f(x)).

Русский

Пусть X и Y — множества, а f: X → Y. Граф графика функции f связывает элемент x ∈ X с элементом y ∈ Y тогда и только тогда, когда y = f(x). Другими словами, графовая релизация f состоит ровно из всех пар (x, f(x)).

LaTeX

$$$ \\forall x \\in X, \\forall y \\in Y: \\ (x,y) \\in \\mathrm{Graph}(f) \\iff y = f(x). $$$

Lean4

@[deprecated rel_graphFunctor_map (since := "2025-06-08")]
theorem graphFunctor_map {X Y : Type u} (f : X ⟶ Y) (x : X) (y : Y) : x ~[(graphFunctor.map f).rel] y ↔ f x = y :=
  .rfl

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