mem_graph_iff — Mathlib

English

An element x = (x1,x2) is in the graph of f iff there exists y in dom(f) with x1 = y and f(y) = x2.

Русский

Элемент x = (x1,x2) принадлежит графу f тогда и только тогда, когда существует y в dom(f) с x1 = y и f(y) = x2.

LaTeX

$$$x \in \mathrm{graph}(f) \iff \exists y : \operatorname{domain}(f), (y, f(y)) = x.$$$

Lean4

@[simp]
theorem mem_graph_iff (f : E →ₗ.[R] F) {x : E × F} : x ∈ f.graph ↔ ∃ y : f.domain, (↑y : E) = x.1 ∧ f y = x.2 :=
  by
  cases x
  simp_rw [mem_graph_iff', Prod.mk_inj]

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