mem_graph_iff' — Mathlib

English

Characterization of membership in the graph via domain elements: x ∈ graph(f) iff there exists y in domain(f) with (↑y, f(y)) = x.

Русский

Характеризация членства в графе через элементы домена: x ∈ graph(f) тогда и только тогда, когда существует y в dom(f) such that (↑y, f(y)) = x.

LaTeX

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

Lean4

theorem mem_graph_iff' (f : E →ₗ.[R] F) {x : E × F} : x ∈ f.graph ↔ ∃ y : f.domain, (↑y, f y) = x := by simp [graph]

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