proj — Mathlib

English

If p corresponds to (f(i), i) in the graph of f, then graph.proj p = f(i).

Русский

Если точка p соответствует кортежу (f(i), i) в графе функции f, то graph.proj p = f(i).

LaTeX

$$$\\text{graph.proj}(p) = f(i)\\text{ if } p = (f(i), i)\\text{ for some } i.$$$

Lean4

/-- Given `p : α ×ₗ (Fin n) := (f i, i)` with `p ∈ graph f`,
`graph.proj p` is defined to be `f i`.
-/
def proj {f : Fin n → α} : graph f → α := fun p => p.1.1

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