Graphs of real-valued functions: membership tests and verifying a finite table as a total function

Goal and scope

(1) Let D=[0,2], f:D→ℝ, f(x)=x²−1. First prove (u,v)∈G_f ⇔ u∈D and v=f(u), then decide whether (1,0), (−1,0), (2,2) and (2,3) lie on G_f. (2) Let D_0={0,1,2} and B={0,1,4}. Prove that a set Γ is the graph of some total function D_0→B exactly when Γ⊆D_0×B and every input has exactly one output; use it to decide that T={(0,0),(1,1),(2,4)} is such a graph, while T_1={(0,0),(2,4)}, T_2={(0,0),(1,1),(1,4),(2,4)} and T_3={(0,0),(1,1),(2,4),(3,9)} are not.

Within the MKO's scope: a fixed Cartesian system, ordered real pairs, and a domain declared first; a total function has exactly one output at each input, and a finite table must also keep its outputs in the declared codomain B. No coordinates are read from sketches, and no inverse, surjectivity or global formula is inferred from finite data; the canonical MKO and its English edition are not changed.

Givens and symbols

• cartesian_product_def
• function_def
• set_builder
• set_extensionality
• order_basics
• numeric_evaluation

• G1 — A Cartesian coordinate system is fixed and points are ordered pairs of reals; the domain is declared first, and a total function has exactly one real output at each input of its domain (MKO assumptions a1, a2).
• G2 — D=[0,2]={x∈ℝ ∣ 0≤x≤2}, f:D→ℝ, f(x)=x²−1; the pairs to test are (1,0), (−1,0), (2,2) and (2,3).
• G3 — D_0={0,1,2} and B={0,1,4}; candidate tables T={(0,0),(1,1),(2,4)}, T_1={(0,0),(2,4)}, T_2={(0,0),(1,1),(1,4),(2,4)} and T_3={(0,0),(1,1),(2,4),(3,9)}.

• D,\ D_0 — declared domains: D=[0,2] and D_0={0,1,2}
• B — the codomain {0,1,4} declared for the finite tables
• G_f=\{(x,f(x))\mid x\in D\} — the graph of f
• T,\ T_1,\ T_2,\ T_3 — four candidate tables (finite sets of ordered pairs)
• \Gamma — a general candidate set of ordered pairs

Rules and sources

• cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
• function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_graph_def · cited — For D⊆R and a total function f:D→R, define G_f={(x,f(x)):x∈D} in a fixed planar Cartesian coordinate system. An ordered pair (u,v) belongs to G_f exactly when u∈D and v=f(u). · mko-function-graph
• mko_table_check · cited — A finite graph may be sorted by first coordinate, listing a repeated ordered pair once. Given D and B, check input by input that there is exactly one output in B, and that there is no graph point outside D; this is the table verification of a specified total function. · mko-function-graph
• L_graph_member · lemma — For any total function f:D→ℝ and reals u, v: (u,v)∈G_f ⇔ u∈D and v=f(u).
• L_table_graph · lemma — For sets D, B⊆ℝ and Γ⊆ℝ²: Γ is the graph of some total function F:D→B exactly when Γ⊆D×B and every u∈D has exactly one v with (u,v)∈Γ.

Main derivation

f:D\to\mathbb{R}\ \text{total},\ D\subseteq\mathbb{R}

G_f=\{(x,f(x))\mid x\in D\}\subseteq\mathbb{R}^2

(u,v)\in G_f

u\in D\ \land\ v=f(u)

(1,0)

1\in D,\ f(1)=1^2-1=0\ \Rightarrow\ (1,0)\in G_f

(-1,0)

-1\notin D\ \Rightarrow\ (-1,0)\notin G_f

(2,2),\ (2,3)

f(2)=3:\ (2,2)\notin G_f,\ (2,3)\in G_f

\Gamma\ \text{is the graph of some total}\ F:D\to B

\Gamma\subseteq D\times B\ \land\ \forall u\in D\ \exists!\,v:\ (u,v)\in\Gamma

T=\{(0,0),(1,1),(2,4)\}

T\subseteq D_0\times B

u\in D_0=\{0,1,2\}

u=0\mapsto 0,\ u=1\mapsto 1,\ u=2\mapsto 4,\ \text{each exactly once}

T\subseteq D_0\times B,\ \forall u\in D_0\ \exists!\,v

T=G_F,\ F:D_0\to B,\ F(0)=0,\ F(1)=1,\ F(2)=4

T_1=\{(0,0),(2,4)\}

\neg\exists v:(1,v)\in T_1\ \Rightarrow\ T_1\ \text{is not the graph of a total}\ D_0\to B

T_2=\{(0,0),(1,1),(1,4),(2,4)\}

(1,1),(1,4)\in T_2,\ 1\neq 4\ \Rightarrow\ T_2\ \text{is not a function graph}

T_3=\{(0,0),(1,1),(2,4),(3,9)\}

(3,9)\notin D_0\times B\ \Rightarrow\ T_3\ \text{is not the graph of a total}\ D_0\to B

\text{four pairs and four tables}

(1,0),(2,3)\in G_f;\ (-1,0),(2,2)\notin G_f;\ T\ \text{accepted};\ T_1,T_2,T_3\ \text{rejected}

Substeps and lemmas

(u,v)\in G_f

u\in D\ \land\ v=f(u)

u\in D\ \land\ v=f(u)

(u,v)=(u,f(u))\in G_f

\Gamma\subseteq D\times B,\ \forall u\in D\ \exists!\,v:(u,v)\in\Gamma

F(u):=\text{the unique}\ v,\quad F:D\to B\ \text{total},\quad G_F=\Gamma

\Gamma=G_F,\ F:D\to B\ \text{total}

\Gamma\subseteq D\times B\ \land\ \forall u\in D\ \exists!\,v:(u,v)\in\Gamma

Reverse audits

• S13 · sufficient_goal_reduction · S03, S04, S05, S09, S10, S11, S12, and_intro_elim — Goal G: the eight decisions. Sufficient condition H: the separate conclusions of S03 to S12; H⇒G is just conjunction. H is proved forwards from the definitions and the two lemmas; G is never used as a premise.
• S12 · premise_audit · S06, contrapositive, cartesian_product_def — 'Exactly one output per input' is only one of the conditions; Γ⊆D×B must hold too.
• S11 · premise_audit · S06, contrapositive — 1≠4 (N9) is enough to break uniqueness; no other input needs checking.
• S10 · premise_audit · S06, contrapositive, G3 — The conclusion concerns the declared D_0 only; T_1 is the graph of a function on {0,2}, but that is a different domain.
• S09 · premise_audit · S06, S07, S08, L_table_graph — Both conditions were proved forwards; the agreement with x² at three points (N8, N11, N12) is an observation, not evidence for a global formula.
• S08 · premise_audit · case_analysis, G3 — The three cases cover every element of D_0; both existence and uniqueness are checked.
• S07 · premise_audit · cartesian_product_def, subset_def — A finite set can be checked element by element; this is a complete check, not a sample.
• S06.2 · premise_audit · S02, function_def — The contrapositive of this direction is the basis for rejecting tables: a missing output, an extra output, or a point outside the domain each rules out being the graph of a total function D→B.
• S06.1 · premise_audit · function_def, set_extensionality, S02 — Existence makes F defined at every point (total), uniqueness makes F a function and gives Γ⊆G_F, and Γ⊆D×B keeps outputs in B with no point outside the domain.
• S06 · inverse_equivalence · L_table_graph, mko_table_check — Both directions of the lemma are proved in the sub-steps, so it may be used as an equivalence; ⇐ accepts T below, and the contrapositive of ⇒ rejects T_1, T_2 and T_3.
• S05 · premise_audit · S02, numeric_evaluation, function_def — u∈D is not enough; v=f(u) must hold as well (N6, N7).
• S04 · premise_audit · S02, order_basics, numeric_evaluation — Failure of one condition is enough for non-membership (N4, N5); the equation alone does not and should not decide it.
• S03 · premise_audit · S02, numeric_evaluation, order_basics — Both conditions are checked (N1, N2, N3); neither may be skipped.
• S02.2 · premise_audit · exists_intro, cartesian_product_def — The witness x=u must lie in D; if u∉D there is no witness even when v equals the value of the formula.
• S02.1 · premise_audit · cartesian_product_def, exists_elim, eq_replace — After naming the witness x, the conclusion no longer mentions x, as ∃-elimination requires.
• S02 · inverse_equivalence · L_graph_member — Both directions of the lemma are proved in the sub-steps, so it may be used as an equivalence.
• S01 · premise_audit · G1, G2, mko_graph_def — This step only states the definition; it uses that f is total, so every x∈D contributes exactly one point.

Error controls and negative controls

Checking only y=f(x) forgets the domain

The first error named in the MKO is to check the equation and forget the domain. (−1,0) satisfies 0=(−1)²−1, but −1∉[0,2], so it is not on G_f (S04). A membership test must check both u∈D and v=f(u) (S02).

The vertical line test is not totality

The second error named in the MKO is to take 'every vertical line meets at most one point' for 'every point of the declared domain has exactly one output'. Each vertical line meets T_1 at most once, but input 1 has no output, so T_1 is not the graph of a total function D_0→B (S10). A full table check must also exclude points outside the domain (S12).

Finite tables do not determine off-domain extensions, and sketches do not replace exact data

T agrees with x² at 0, 1 and 2, but this gives no formula for F elsewhere; F is defined only on D_0 (S09). A sketch provides no exact coordinates, and finite data do not by themselves establish an inverse or surjectivity (MKO para2).

• (−1,0)∈G_f because (−1)²−1=0 → reject — −1∉D=[0,2]; membership also requires the first coordinate to lie in the domain.
• (2,2)∈G_f because 2∈D → reject — f(2)=3≠2; the second coordinate must equal f(2).
• T_1={(0,0),(2,4)} passes the vertical line test, so it is the graph of a total function D_0→B → reject — 1∈D_0 has no output; the vertical line test does not check totality.
• T_3 has exactly one output at every input of D_0, so it is the graph of a total function D_0→B → reject — T_3 contains (3,9) with 3∉D_0 and 9∉B, so T_3⊄D_0×B.
• T agrees with x² at 0, 1 and 2, so F is the function x² on ℝ → reject — F is defined only on D_0; finite data determine neither values outside the domain nor a global formula.

Result and limitations

(u,v)∈G_f exactly when u∈D and v=f(u). For D=[0,2] and f(x)=x²−1: (1,0) and (2,3) lie on the graph; (−1,0) does not (−1∉D, although the formula gives 0); (2,2) does not (f(2)=3). A set is the graph of a total function D_0→B exactly when it is a subset of D_0×B and every input has exactly one output: T={(0,0),(1,1),(2,4)} is one; T_1 lacks an output at 1 (though it passes the vertical line test), T_2 has two outputs at 1, and T_3 has the extra point (3,9), so none of these is.

• This guide does not discuss geometric properties of graphs (continuity, shape), and infers no inverse or surjectivity from a graph.
• N8, N11 and N12 only record that x² takes the values 0, 4 and 1 at 0, 2 and 1, matching the outputs of T there; they support no global formula.

Verification and source binding

12 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: fd7c2071f9e6afa63b288de5141c6fb96961f0e1fe8adfbf5194e5cf438c7930
• original source SHA-256: 0b42b0a6e4a678932e19deb35bc9d4abbca16e6381f1a4c619ddbdb34f21a2b6
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)