All public logs
Jump to navigation
Jump to search
Combined display of all available logs of ProofWiki. You can narrow down the view by selecting a log type, the username (case-sensitive), or the affected page (also case-sensitive).
- 00:27, 29 April 2024 CircuitCraft talk contribs created page Inner Jordan Content is Well-Defined (Created page with "== Theorem == Let $M \subseteq \R^n$ be a bounded subspace of Euclidean $n$-space. Let: :$\ds R = \prod_{i \mathop = 1}^n \closedint {a_i} {b_i}$ :$\ds R' = \prod_{i \mathop = 1}^n \closedint {a'_i} {b'_i}$ be closed $n$-rectangles that contain $M$. Let $V_R, V_{R'} \in \R_{\ge 0}$ be defined as: :$\ds V_R = \prod_...")
- 06:43, 28 April 2024 CircuitCraft talk contribs created page Outer Jordan Content of Dilation (Created page with "== Theorem == Let $M \subseteq \R^n$ be a bounded subspace of Euclidean $n$-space. Let $c_1, c_2, \dotsc, c_n \in \R_{\ge 0}$ be non-negative real numbers. Let $M' \subseteq \R^n$ be defined as: :$M' = \set {\tuple {c_1 x_1, c_2 x_2, \dotsc, c_n x_n} : \tuple {x_1, x_2, \dotsc, x_n} \in \R^n}$ Then: :$\map {m^*} {M'} = c_1 c_2 \dotsm c...")
- 04:32, 28 April 2024 CircuitCraft talk contribs created page Set of Intersections with Superset is Cover (Created page with "== Theorem == Let $S$ be a set. Let $\CC$ be a cover of $S$. Let $T \supseteq S$ be a superset of $S$. Then: :$\set {C \cap T : C \in \CC}$ is a cover of $S$. == Proof == Let $x \in S$ be arbitrary. By definition of cover, there is some $C \in \CC$ such that: :$x \in C$ By definition of superset: :$x \in T$ Ther...")
- 03:45, 28 April 2024 CircuitCraft talk contribs created page Jordan Content is Monotone (Created page with "== Theorem == Let $A, B \subseteq \R^n$ be bounded subspaces of Euclidean $n$-space. Suppose that $A \subseteq B$. Further suppose that the Jordan content of both $A$ and $B$ exists. Then: :$\map m A \le \map m B$ where $m$ denotes the Jordan content. == Proof == By definition of the Definition:Jordan Content|J...")
- 03:24, 28 April 2024 CircuitCraft talk contribs created page Outer Jordan Content is Subadditive (Created page with "== Theorem == Let $A, B \subseteq \R^n$ be bounded subspaces of Euclidean $n$-space. Then: :$\map {m^*} {A \cup B} \le \map {m^*} A + \map {m^*} B$ where $m^*$ denotes the outer Jordan content. == Proof == Let $\epsilon > 0$ be arbitrary. By Characterizing Property of Infimum of Subset of Real Numbers, select: :$C$ to be a Definiti...")
- 22:21, 27 April 2024 CircuitCraft talk contribs created page Union of Covers is Cover of Union (Created page with "== Theorem == Let $\sequence {S_i}_{i \in I}$ be an indexed family of sets. For each $i \in I$, let $\CC_i$ be a cover of $S_i$. Then, $\ds \bigcup_{i \mathop \in I} \CC_i$ is a cover of $\ds \bigcup_{i \mathop \in I} S_i$. == Proof == Let $\ds x \in \bigcup_{i \mathop \in I} S_i$ be arbitrary. By definition of union, there is some $i \in I...")
- 20:22, 27 April 2024 CircuitCraft talk contribs created page Inner Jordan Content is Monotone (Created page with "== Theorem == Let $A, B \subseteq \R^n$ be bounded subspaces of Euclidean $n$-space. Suppose that $A \subseteq B$. Then: :$\map {m_*} A \le \map {m_*} B$ where $m_*$ denotes the inner Jordan content. == Proof == Let $R \subseteq \R^n$ be a closed $n$-rectangle that contains $...")
- 20:03, 27 April 2024 CircuitCraft talk contribs created page Outer Jordan Content is Monotone (Created page with "== Theorem == Let $A, B \subseteq \R^n$ be bounded subspaces of Euclidean $n$-space. Suppose that $A \subseteq B$. Then: :$\map {m^*} A \le \map {m^*} B$ where $m^*$ denotes the outer Jordan content. == Proof == Let $C$ be a finite covering of $B$ by closed rectangles. Since $A...")
- 19:54, 27 April 2024 CircuitCraft talk contribs created page Cover is Cover of Subset (Created page with "== Theorem == Let $S$ be a set. Let $\CC$ be a cover of $S$. Let $T \subseteq S$ be a subset of $S$. Then, $\CC$ is a cover of $T$. == Proof == By definition of a cover: :$\ds S \subseteq \bigcup C$ But then, by Subset Relation is Transitive: :$\ds T \subseteq \bigcup C$ Therefore, $C$ is a cover of $T$ by...")
- 17:56, 27 April 2024 CircuitCraft talk contribs created page Definition:Inner Jordan Content (Created page with "== Definition == Let $M \subseteq \R^n$ be a bounded subspace of Euclidean $n$-space. Let $R \subseteq \R^n$ be closed $n$-rectangle that contains $M$. Then, the '''inner Jordan content''' of $M$ is defined and denoted as: :$\map {m_*} M = \map V R - \map {m^*} {R \setminus M}$ where: :$\map V R$ denotes: ::$\ds \m...")
- 03:00, 26 April 2024 CircuitCraft talk contribs created page Limit to Infinity of Binomial Coefficient over Power/Proof 2 (Created page with "== Theorem == {{:Limit to Infinity of Binomial Coefficient over Power}} == Proof == <onlyinclude> This proof applies to the special case where $k \in \Z$. Then, {{hypothesis}}, we need only consider: :$k \in \set {0, 1, 2, \dotsc}$ By Gamma Function Extends Factorial, it suffices to show: :$\ds \lim_{r \mathop \to \infty} \frac {\dbinom r k} {r^k} = \frac 1 {k !}$ We have: {{begin-eqn}} {{eqn | q = \forall r \in \R | l = \frac {\dbinom r k} {r^k} |...")
- 02:14, 26 April 2024 CircuitCraft talk contribs created page Limit to Infinity of Binomial Coefficient over Power/Proof 1 (Created page with "== Theorem == {{:Limit to Infinity of Binomial Coefficient over Power}} == Proof == <onlyinclude> {{begin-eqn}} {{eqn | l = \lim_{r \mathop \to \infty} \frac {\dbinom r k} {r^k} | r = \lim_{r \mathop \to \infty} \frac {\map \Gamma {r + 1} } {\map \Gamma {k + 1} \map \Gamma {r - k + 1} r^k} | c = Gamma Function Extends Factorial }} {{eqn | r = \lim_{r \mathop \to \infty} \frac 1 {\map \Gamma {k + 1} } \frac {\sqrt {2 \pi r} \paren {r / e}^r} {\sqrt {2 \p...")
- 02:53, 24 April 2024 CircuitCraft talk contribs created page Principle of Open Induction for Real Numbers (Created page with "== Theorem == Let $a < b$ be real numbers. Let $S$ be an open set of real numbers. Suppose that, for every $x \in \closedint a b$ such that: :$\hointr a x \subseteq S$ it also holds that: :$x \in S$ Then, $\closedint a b \subseteq S$. == Proof == {{AimForCont}} there exists some $x \in \closedint a b$ such that: :$x \notin S$ Let: :$T := \closedint a b \setminus S$ be the set o...")
- 23:37, 25 March 2024 CircuitCraft talk contribs created page Filter Containing Complements is Not Proper (Created page with "== Theorem == Let $L = \struct {S, \lor, \land, \preceq}$ be a bounded lattice. Let $F \subseteq S$ be a filter on $L$. Suppose there exist $a, b \in F$ such that: :$b$ is a complement of $a$ Then, $F = S$. == Proof == By filter axiom $\paren 2$: :$\exists c \in F: c \preceq a \land c \preceq b$ By definition of Definition:Complement (Lattice...")
- 16:57, 21 March 2024 CircuitCraft talk contribs created page Riemann-Stieltjes Integral with Step Integrator (Created page with "== Theorem == Let $a < c < b$ be real numbers. Let $f$ be a real function that is bounded on $\closedint a b$. Let $\alpha$ be a real function on $\closedint a b$ such that: :$\forall x \in \hointr a c: \map \alpha x = \map \alpha a$ :$\forall x \in \hointl c b: \map \alpha x = \map \alpha b$ Suppose that: :Either $f$ is Definition:Left-C...")
- 05:16, 21 March 2024 CircuitCraft talk contribs created page Continuous at Point iff Left-Continuous and Right-Continuous (Created page with "== Theorem == Let $A \subseteq \R$ be an open set of real numbers. Let $f : A \to \R$ be a real function. Let $x_0 \in A$. Then: :$f$ is continuous at $x_0$ {{iff}}: :$f$ is both left-continuous and right-continuous at $x_0$ == Proof == === Necessary Condition === Su...")
- 02:24, 21 March 2024 CircuitCraft talk contribs created page Integration by Substitution/Riemann-Stieltjes Integral/Decreasing (I don't see an easy way to derive this from the Increasing case.)
- 01:34, 21 March 2024 CircuitCraft talk contribs moved page Integration by Substitution/Riemann-Stieltjes Integral to Integration by Substitution/Riemann-Stieltjes Integral/Increasing (Special case of general theorem ($g$ is monotone).)
- 01:18, 21 March 2024 CircuitCraft talk contribs created page Reduction of Riemann-Stieltjes Integral to Identity Integrator (We don't have good coverage for one-sided derivatives, etc., which is what is meant here.)
- 00:58, 21 March 2024 CircuitCraft talk contribs moved page Sum of Riemann-Stieltjes Integrals on Adjacent Intervals/Part to Sum of Riemann-Stieltjes Integrals on Adjacent Intervals/Whole to Part without leaving a redirect (More descriptive name)
- 00:57, 21 March 2024 CircuitCraft talk contribs moved page Sum of Riemann-Stieltjes Integrals on Adjacent Intervals/Whole to Sum of Riemann-Stieltjes Integrals on Adjacent Intervals/Part to Whole without leaving a redirect (Better naming convention.)
- 07:05, 20 March 2024 CircuitCraft talk contribs created page Talk:Sum of Riemann-Stieltjes Integrals on Adjacent Intervals (Created page with "Subpages are transcluded lower down the page as lemmata. --~~~~")
- 06:05, 20 March 2024 CircuitCraft talk contribs created page Existence of Subdivision with Small Norm (Created page with "== Theorem == Let $\closedint a b$ be a closed real interval. Let $\epsilon > 0$ be a positive real number. Then, there exists a finite subdivision $P$ of $\closedint a b$ such that: :$\norm P < \epsilon$ where $\norm P$ denotes the norm of $P$. == Proof == By the Axiom of Archimedes, choose $N \in \N$ such that:...")
- 05:29, 20 March 2024 CircuitCraft talk contribs created page Norm of Refinement is no Greater than Norm of Subdivision (Created page with "== Theorem == Let $P$ be a finite subdivision of $\closedint a b$. Let $P'$ be a refinement of $P$. Then: :$\norm {P'} \le \norm P$ where $\norm P$ denotes the norm of $P$. == Proof == Let $P = \set {x_0, x_1, \dotsc, x_{n - 1}, x_n}$. Let $P' = \set {y_0, y_1, \dotsc, y_{m - 1}, y_m}$. By definition of Definition:Refinement of Finite Subdivision...")
- 04:27, 20 March 2024 CircuitCraft talk contribs created page Riemann-Stieltjes Integral by Norm of Subdivision/Riemann Integral (Created page with "== Theorem == <onlyinclude> Let $f$ be a real function that is bounded on $\closedint a b$. Suppose $f$ is Riemann integrable on $\closedint a b$. Let $\iota$ be the identity mapping on $\closedint a b$. Then, $f$ is Riemann-Stieltjes integrable with respect to $\iota$ on $\closedint a b$ an...")
- 03:57, 20 March 2024 CircuitCraft talk contribs created page Riemann-Stieltjes Integral by Norm of Subdivision (Created page with "== Theorem == Let $f, \alpha$ be real functions that are bounded on $\closedint a b$. Suppose there exists some $A \in \R$ where, for every $\epsilon > 0$, there exists some $\delta_\epsilon > 0$ such that: :For every finite subdivision $P$ of $\closedint a b$, if the norm $\norm P < \delta_\epsilon$, then: ::For every Definiti...")
- 02:34, 20 March 2024 CircuitCraft talk contribs created page Sum of Riemann-Stieltjes Integrals on Adjacent Intervals (Created page with "== Theorem == Let $a, b, c \in \R$. Let $f, \alpha$ be real functions that are bounded on some closed interval containing $a, b, c$. Suppose that two of the following three Riemann-Stieltjes integrals exist, with the limits of integration interpreted in the Definition:Riemann-Stieltjes Integral/General Limits of Integ...")
- 02:10, 20 March 2024 CircuitCraft talk contribs moved page Definition:Riemann-Stieltjes Integral/General Bounds to Definition:Riemann-Stieltjes Integral/General Limits of Integration without leaving a redirect (I messed up my terminology.)
- 01:52, 20 March 2024 CircuitCraft talk contribs created page Definition:Riemann-Stieltjes Integral/General Bounds (Created page with "== Definition == <onlyinclude> The notation for the Riemann-Stieltjes integral: :$\ds A = \int_a^b f \rd \alpha = \int_a^b \map f x \rd \map \alpha x$ is defined for $a < b$. We extend it to arbitrary $a, b \in \R$ by the following conventions. If $a = b$, then: :$\ds \int_a^b f \rd \alpha = \int_a^b \map f x \rd \map \alpha x := 0$ If $a > b$, then: :$\ds \int_a^b f \rd \alpha = \int_a^b \map f x \rd \map \alpha x := - \int...")
- 01:41, 20 March 2024 CircuitCraft talk contribs created page Sum of Riemann-Stieltjes Integrals on Adjacent Intervals/Part (Created page with "== Theorem == <onlyinclude> Let $a < c < b$ be real numbers. Let $f, \alpha$ be real functions that are bounded on $\closedint a b$ Suppose that $f$ is Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a b$, and also on one of the two intervals $\closedint a c$ and $\closedin...")
- 00:53, 20 March 2024 CircuitCraft talk contribs created page Sum of Riemann-Stieltjes Integrals on Adjacent Intervals/Whole (Created page with "== Theorem == <onlyinclude> Let $a < c < b$ be real numbers. Let $f, \alpha$ be real functions that are bounded on $\closedint a b$ Suppose that $f$ is Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a c$, and also on $\closedint c b$. Then, $f$ is Definition:Riemann-Stieltjes Integral|Riemann-Stieltjes i...")
- 22:50, 19 March 2024 CircuitCraft talk contribs created page Riemann-Stieltjes Integral of Constant Integrand (Created page with "== Theorem == Let $\alpha$ be a real function that is bounded on $\closedint a b$. Let $f : \closedint a b \to \R$ be defined as: :$\map f x = c$ for some $c \in \R$. Then, $f$ is Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a b$, and: :$\int_a^b f \rd \alpha = c \map \alpha b - c \map \alpha a$ == Proof == Let $\epsilon > 0$...")
- 21:46, 19 March 2024 CircuitCraft talk contribs created page Integration by Substitution/Riemann-Stieltjes Integral (Created page with "== Theorem == Let $g$ be a real function that is continuous and strictly increasing on $\closedint a b$. Let $f, \alpha$ be real functions that are bounded on $\closedint {\map g a} {\map g b}$. Further suppose that $f$ is Definition:Riemann-Stieltjes Integral|Riemann-...")
- 20:41, 19 March 2024 CircuitCraft talk contribs created page Definition talk:Riemann-Stieltjes Integral (Created page with "Combining '''integrable''' and '''integral''' on the same page is done in both Definition:Riemann Integral and Definition:Darboux Integral, so I figured it wouldn't be a problem here. If we're splitting them here, we should do the same on those pages for consistency. --~~~~")
- 07:40, 19 March 2024 CircuitCraft talk contribs created page Integration by Parts/Riemann-Stieltjes Integral (Created page with "== Theorem == Let $f, \alpha$ be a real functions that are bounded on $\closedint a b$. Suppose that $f$ is Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a b$. Then, $\alpha$ is Riemann-Stieltjes integrable with respect to $f$ on $\closedint a b$ and: :$\ds \int_a^b f \rd \alpha + \int_a^b...")
- 06:04, 19 March 2024 CircuitCraft talk contribs created page Linear Combination of Riemann-Stieltjes Integrals/Integrator (Created page with "== Theorem == Let $f, \alpha, \beta$ be a real functions that are bounded on $\closedint a b$. Let $c_1, c_2 \in \R$. Suppose that $f$ is Riemann-Stieltjes integrable with respect both $\alpha$ and $\beta$ on $\closedint a b$ and: :$\ds \int_a^b f \rd \alpha = A$ :$\ds \int_a^b f \rd \beta = B$ Then, $f$ is Definition:Riemann-Stieltjes Integral|Rieman...")
- 05:37, 19 March 2024 CircuitCraft talk contribs created page Linear Combination of Riemann-Stieltjes Integrals/Integrand (Created page with "== Theorem == Let $f, g, \alpha$ be a real functions that are bounded on $\closedint a b$. Let $c_1, c_2 \in \R$. Suppose that $f$ and $g$ are Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a b$ and: :$\ds \int_a^b f \rd \alpha = A$ :$\ds \int_a^b g \rd \alpha = B$ Then, the real function $h : \closedin...")
- 04:47, 19 March 2024 CircuitCraft talk contribs created page Definition:Riemann-Stieltjes Integral (Created page with "== Definition == Let $\Bbb I = \closedint a b$ be a closed real interval. Let $f, \alpha : \Bbb I \to \R$ be a real functions that are bounded on $\Bbb I$. Then, $f$ is '''Riemann-Stieltjes integrable''' with respect to $\alpha$ on $\closedint a b$ {{iff}}: :There exists some $A \in \R$ such that, for every $\epsilon > 0$, there is a Definition:Finite Subdiv...")
- 04:27, 19 March 2024 CircuitCraft talk contribs created page Definition:Riemann-Stieltjes Sum (Created page with "== Definition == Let $\Bbb I = \closedint a b$ be a closed real interval. Let $f, \alpha : \Bbb I \to \R$ be a real functions that are bounded on $\Bbb I$. Let $P = \set {x_0, x_1, \dotsc, x_n}$ be a finite subdivision of $\closedint a b$. For each $k \in \set {1, \dotsc, n}$, let $t_k \in \closedint {x_{k - 1}} {x_k}$. Then...")
- 05:54, 26 February 2024 CircuitCraft talk contribs created page Existence of Middle Universal Product/Corollary (Created page with "== Corollary to Existence of Middle Universal Product == <onlyinclude> For each $n \in \N_{> 0}$ and $m \in \N$, the following is a theorem of von Neumann-Bernays-Gödel set theory: :$\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x_1, \dotsc, x_n: \forall y: \sequence {x_1, \dotsc, x_n, v_1, \dotsc, v_m, y} \in Z \iff \sequence {x_1, \dotsc, x_n, y} \in X$ </onlyinclude> where the n...")
- 04:36, 26 February 2024 CircuitCraft talk contribs created page Existence of Middle Universal Product/Lemma (Created page with "== Lemma for Existence of Middle Universal Product == <onlyinclude> The following is a theorem of von Neumann-Bernays-Gödel set theory: :$\forall X: \exists Z: \forall u, v, w: \tuple {\tuple {u, v}, w} \in Z \iff \tuple {u, w} \in X$ </onlyinclude> == Proof == Let $X$ be arbitrary. By Axiom $\text B 5$, there exists some class $Z$...")
- 04:16, 26 February 2024 CircuitCraft talk contribs created page Existence of Middle Universal Product (Created page with "== Theorem == For each $m \in \N$, the following is a theorem of von Neumann-Bernays-Gödel set theory: :$\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x, y: $\sequence {x, v_1, \dotsc, v_m, y} \in Z \iff $\tuple {x, y} \in X$ where the notation $\sequence {\cdot, \dotsc, \cdot}$ is defined inductively as: :$\sequence {y_1} := y_1$ :$\sequence {y_1, \dotsc, y_k, y_{k + 1}} := \tuple {\...")
- 04:03, 26 February 2024 CircuitCraft talk contribs created page Existence of Left Universal Product (Created page with "== Theorem == For each $m \in \N_{> 0}$, the following is a theorem of von Neumann-Bernays-Gödel set theory: :$\forall X: \exists Z: \forall x: \forall v_1, \dotsc, v_m: \sequence {v_1, \dotsc, v_m, x} \in Z \iff x \in X$ where the notation $\sequence {\cdot, \dotsc, \cdot}$ is defined inductively as: :$\sequence {y_1} := y_1$ :$\sequence {y_1, \dotsc, y_k, y_{k + 1}} := \tuple {\sequence {y_1,...")
- 03:14, 26 February 2024 CircuitCraft talk contribs created page Existence of Right Universal Product/Corollary (Created page with "== Corollary to Existence of Right Universal Product == <onlyinclude> For all $n \in \N_{> 0}$ and $m \in \N$, the following is a theorem of von Neumann-Bernays-Gödel set theory: :$\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x_1, \dotsc, x_n: \sequence {x_1, \dotsc, x_n, v_1, \dotsc, v_m} \in Z \iff \sequence{x_1, \dotsc, x_n} \in X$ where the notation $\sequence {\cdot, \dotsc,...")
- 01:55, 26 February 2024 CircuitCraft talk contribs created page Existence of Right Universal Product (Created page with "== Theorem == For each $m \in \N$, the following is a theorem of von Neumann-Bernays-Gödel set theory: :$\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x: \tuple {\tuple {\dots \tuple {x, v_1}, \dots}, v_m} \in Z \iff x \in X$ Informally, for any class $X$, there is some class $Z$ such that: :$Z = \paren {\dotsm \paren {X \times V} \times \do...")
- 20:16, 25 February 2024 CircuitCraft talk contribs created page Existence of Inverse of Class Relation (Created page with "== Theorem == Let $X$ be a class. Then there is a class $Z$ such that, for all sets $u, v$: :$\tuple {u, v} \in Z \iff \tuple {v, u} \in X$ where $\tuple {\cdot, \cdot}$ denotes the Kuratowski formalization of ordered pairs. == Proof == Let $X$ be arbitrary. By Axiom $\text B 5$, there is a Definition:Class|class...")
- 07:28, 25 February 2024 CircuitCraft talk contribs created page Existence of Universal Class (Created page with "== Theorem == There exists a unique class $V$ such that: :$\forall u: u \in V$ That is, the universal class exists and is unique. == Proof == By Existence of Empty Class, there is a unique class $\O$ such that: :$\forall u: u \notin \O$ for every set $u$. Thus, by Existence of Class Complement, there i...")
- 07:20, 25 February 2024 CircuitCraft talk contribs created page Existence of Class Union (Created page with "== Theorem == For any classes $X, Y$, the union $X \cup Y$ exists and is unique. That is: :$\forall X, Y: \exists! Z: \forall u: u \in Z \iff u \in X \lor u \in Y$ where $X \cup Y := Z$. == Proof == By Existence of Class Complement, there exist unique classes $\overline X, \overline Y$ such that: :$u \in \overline X \iff u \notin X$ :$u \in \overline...")
- 07:04, 25 February 2024 CircuitCraft talk contribs created page Existence of Domain of Class Relation (Created page with "== Theorem == Let $X$ be a class. Then there is a unique class $Z$ such that: :$\forall u: u \in Z \iff \exists v: \tuple {u, v} \in X$ where $\tuple {\cdot, \cdot}$ represents the Kuratowski formalization of ordered pairs. That is, $Z$ is the class of all $z$ which appear as the Definition:Coordinate of Ordered Pair|first coor...")
- 22:28, 23 February 2024 CircuitCraft talk contribs created page Axiom:Axiom of Global Choice (Created page with "== Axiom == In the context of class theory, the '''axiom of global choice''' is as follows: <onlyinclude> There exists a mapping $f : V \setminus \set \O \to V$, where $V$ is the universal class, such that: :$\forall x \in V: \map f x \in x$ Symbolically: :$\exists A: \map {\text{Fnc}} A \land \forall x: x \ne \O \implies \exists y: y \in x \land \tuple {x, y} \in A$ </onlyi...")