nyuuzyou/wikis huggingface dataset:
Projection is Surjection/Family of Sets

== Theorem ==
Let $\family {S_\alpha}_{\alpha \mathop \in I}$ be a family of sets.
Let $\ds \prod_{\alpha \mathop \in I} S_\alpha$ be the Cartesian product of $\family {S_\alpha}_{\alpha \mathop \in I}$.
Let each of $S_\alpha$ be non-empty.
For each $\beta \in I$, let $\ds \pr_\beta: \prod_{\alpha \mathop \in I} S_\alpha \to S_\beta$ be the $\beta$th projection on $\ds S = \prod_{\alpha \mathop \in I} S_\alpha$.
Then $\pr_\beta$ is a surjection.
== Proof ==
Consider the $\beta$th projection.
Let $x_\beta \in S_\beta$.
Let $\map x \beta = x_\beta$
Suppose $\gamma \in I: \gamma \ne \beta$.
As $S_\gamma \ne \O$ it is possible to use the axiom of choice to choose $\map x \gamma \in S_\gamma$.
Then:
:$\ds x \in \prod_{\alpha \mathop \in I} S_\alpha$
and:
:$\map {\pr_\beta} x = \map x \beta$
Hence the result.
== Sources ==
* : Chapter $1$: Theory of Sets: $\S 10$: Arbitrary Products
Category:Surjections
Category:Indexed Families
Category:Projections
Projection is Surjection/General Version

== Theorem ==
For all non-empty sets $S_1, S_2, \ldots, S_j, \ldots, S_n$, the $j$th projection $\pr_j$ on $\ds \prod_{i \mathop = 1}^n S_i$ is a surjection.
== Proof ==
Consider the $j$th projection.
As long as none of $S_1, S_2, \ldots, S_n$ is the empty set, then:
:$\ds \forall x \in S_j: \exists \tuple {s_1, s_2, \ldots, s_{j - 1}, x, s_{j + 1}, \ldots, s_n} \in \prod_{k \mathop = 1}^n S_k: \map {\pr_j} {\tuple {s_1, s_2, \ldots, s_{j - 1}, x, s_{j + 1}, \ldots, s_n} } = x$
Hence the result.
Category:Surjections
Category:Projections
Projection of Complement Contains Complement of Projection

== Theorem ==
Let $S$ and $T$ be non-empty sets.
Let $X \subseteq S \times T$ be a subset of the Cartesian product $S \times T$.
Denote with $\pr_1, \pr_2$ and $\complement$ the first and second projections, and the complement operation, respectively.
Then:
== Proof ==
Let $s \in S$.
Then:
In conclusion:
:$s \in \map \complement {\map {\pr_1} X} \implies s \in \map {\pr_1} {\map \complement X}$
and by definition of subset, the first relation follows.
Mutatis mutandis the other relation can be established.
Category:Projections
Category:Set Complement
Projection of Conic Section is Conic Section/Historical Note

== Historical Note on Projection of Conic Section is Conic Section ==
 developed the concept of the conic section in the context of projective geometry.
Hence he was able to demonstrate Projection of Conic Section is Conic Section.
This was widely disregarded at the time, caused in part by the obscure terminology he used, but also because the influence of projective geometry was overshadowed by the contemporary development of analytic geometry.
== Sources ==
* 
* 
Category:Historical Notes
Projection of Euclidean Space onto Euclidean Subspace is Riemannian Submersion

== Theorem ==
Let $\struct {\R^{n + k}, g^E_{n + k}}$, $\struct {\R^n, g^E_n}$ be the real vector spaces with Euclidean metrics.
Let $\pi : \R^{n + k} \to \R^n$ be the projection onto the first $n$ coordinates.
Then $\pi$ is a Riemannian submersion.
== Proof ==
== Sources ==
* : $\S 2$: Riemannian Metrics. Methods for Constructing Riemannian Metrics
Category:Riemannian Geometry
Projection of Product Manifold onto Factor Manifold is Riemannian Submersion

== Theorem ==
Let $\struct {M, g^M}$ and $\struct {N, g^N}$ be Riemannian manifolds.
Let $M \times N$ be the product manifold endowed with the product metric $g = g^M \oplus g^N$.
Let $\pi_M$, $\pi_N$ be projections such that:
:$\pi_M : M \times N \to M$
:$\pi_N : M \times N \to N$
Then $\pi_M$ and $\pi_N$ are Riemannian submersions.
== Proof ==
== Sources ==
* : $\S 2$: Riemannian Metrics. Methods for Constructing Riemannian Metrics
Category:Riemannian Geometry
Projection of Subset is Open iff Saturation is Open

== Theorem ==
Let $\sim$ be an equivalence relation on a topological space $\struct {X, \tau}$.
Let $p$ denote the quotient mapping induced by $\sim$.
Let $\tau_\sim$ be the quotient topology on $X / \sim$ by $p$.
Let $\struct {X / \sim, \tau_\sim}$ be the quotient space of $X$ by $\sim$.
Let $U \subset X$.
Then the following are equivalent:
:$\map p U$ is open in $\struct {X / \sim, \tau_\sim}$
:The saturation of $U$ is open in $\struct {X, \tau}$
== Proof 1==
By definition of quotient topology, $\map p U$ is open in $\struct {X / \sim, \tau_\sim}$ $\map {p^{-1} } {\map p U}$ is open in $\struct {X, \tau}$.
== Proof 2==
===Neccessary Condition===
We are given that:
:$\map p U$ is open in $\struct {X / \sim, \tau_\sim}$
So:
:$\map p U \in \tau_\sim$
We are given that $p$ is the quotient mapping induced by $\sim$, so:
:$\overline U = p^{-1} \sqbrk {p \sqbrk U} \in \tau$
Hence:
:The saturation of $U$ is open in $\struct {X, \tau}$
===Sufficient Condition===
We are given that:
:The saturation of $U$ is open in $\struct {X, \tau}$
We are given that $p$ is the quotient mapping induced by $\sim$, so:
:$\overline U = p^{-1} \sqbrk {p \sqbrk U} \in \tau$
So:
:$\map p U \in \tau_\sim$
Hence:
:$\map p U$ is open in $\struct {X / \sim, \tau_\sim}$
Hence the result
== Also see ==
* Group Acts by Homeomorphisms Implies Projection on Quotient Space is Open
Category:Quotient Spaces
Projection of Warped Product Manifold onto Unwarped Factor Manifold is Riemannian Submersion

== Theorem ==
Let $\struct {M, g^M}$ and $\struct {N, g^N}$ be Riemannian manifolds.
Let $f : M \to \R_{\mathop > 0}$ be a strictly positive smooth function.
Let $M \times_f N$ be the warped product manifold endowed with the metric $g = g^M \oplus f^2 g^N$.
Let $\pi_M$, $\pi_N$ be projections such that:
:$\pi_M : M \times_f N \to M$
:$\pi_N : M \times_f N \to N$
Then $\pi_M$ is a Riemannian submersion, but $\pi_N$ is not necessarily so.
== Proof ==
== Sources ==
* : $\S 2$: Riemannian Metrics. Methods for Constructing Riemannian Metrics
Category:Riemannian Geometry
Projection on Cartesian Product of Modules

== Theorem ==
Let $\struct {R, +_R, \times_R}$ be a ring.
Let $\struct {G, +, \circ}_R$ be the cartesian product of a sequence $\sequence {\struct {G_n, +_n, \circ_n}_R}$ of $R$-modules.
Then for each $j \in \closedint 1 n$, the projection $\pr_j$ on the $j$th co-ordinate is an epimorphism from $\struct {G, +, \circ}_R$ onto $\struct {G_j, +_j, \circ_j}_R$.
== Proof ==
To demonstrate that $\pr_j$ is an epimorphism, we need to show that:
:$(1): \quad \pr_j$ is a surjection
:$(2): \quad \forall x, y \in G: \map {\pr_j} {x + y} = \map {\pr_j} x +_j \map {\pr_j} y$
:$(3): \quad \forall x \in G: \forall \lambda \in R: \map {\pr_j} {\lambda \circ x} = \lambda \circ_j \map {\pr_j} x$
Criteria $(1)$ and $(2)$ are a direct application of Projection is Epimorphism.
Let $x = \tuple {x_1, x_2, \ldots, x_j, \ldots, x_n}$
Then we have:
== Sources ==
* : Chapter $\text {V}$: Vector Spaces: $\S 28$. Linear Transformations: Example $28.7$
Category:Cartesian Product
Category:Projections
Category:Epimorphisms (Abstract Algebra)
Category:Module Theory
Projection on Group Direct Product is Epimorphism

== Theorem ==
Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups.
Let $\struct {G, \circ}$ be the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$.
Then:
:$\pr_1$ is an epimorphism from $\struct {G, \circ}$ to $\struct {G_1, \circ_1}$
:$\pr_2$ is an epimorphism from $\struct {G, \circ}$ to $\struct {G_2, \circ_2}$
where $\pr_1$ and $\pr_2$ are the first and second projection respectively of $\struct {G, \circ}$.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : Chapter $\text{II}$: Groups: Direct Products
* : Chapter $8$: Homomorphisms, Normal Subgroups and Quotient Groups: Exercise $5$
Category:Group Epimorphisms
Category:Group Direct Products
Category:Projection on Group Direct Product is Epimorphism
Projection on Group Direct Product is Epimorphism/Proof 1

== Theorem ==
== Proof ==
From Projection is Surjection, $\pr_1$ and $\pr_2$ are surjections.
We now need to show they are homomorphisms.
Let $g, h \in \struct {G, \circ}$ where $g = \tuple {g_1, g_2}$ and $h = \tuple {h_1, h_2}$.
Then:
and thus the morphism property is demonstrated for both $\pr_1$ and $\pr_2$.
Category:Projection on Group Direct Product is Epimorphism
Projection on Real Euclidean Plane is Open Mapping

== Theorem ==
Let $\struct {\R^2, d}$ be the real number plane with the usual (Euclidean) topology.
Let $\rho: \R^2 \to \R$ be the first projection on $\R^2$ defined as:
:$\forall \tuple{x, y} \in \R^2: \map \rho {x, y} = x$
Then $\rho$ is an open mapping.
The same applies with the second projection on $\R^2$.
== Proof ==
By definition, the real number plane with the usual (Euclidean) topology on $\R^2$ is the product space of $\struct {\R, d}$ with $\struct {\R, d}$, where $\struct {\R, d}$ is the real number line with the usual (Euclidean) topology
The result follows from Projection from Product Topology is Open.
== Sources ==
* : Part $\text {II}$: Counterexamples: $33$. Special Subsets of the Plane: $1$
Category:Real Number Plane with Euclidean Topology
Category:Open Mappings
Projection on Real Euclidean Plane is not Closed Mapping

== Theorem ==
Let $\struct {\R^2, d}$ be the real number plane with the usual (Euclidean) topology.
Let $\rho: \R^2 \to \R$ be the first projection on $\R^2$ defined as:
:$\forall \tuple {x, y} \in \R^2: \map \rho {x, y} = x$
Then $\rho$ is not a closed mapping.
The same applies with the second projection on $\R^2$.
== Proof ==
Consider the set $A \subseteq R^2$ of all points defined as:
:$A := \set {\tuple {x, y} \in \R^2: x y \ge 1}$
By Subset of Euclidean Plane whose Product of Coordinates are Greater Than or Equal to 1 is Closed:
:$A$ is a closed set in $\struct {\R^2, d}$.
By inspection, it can be seen that the image of $A$ under $\rho$ is:
:$\rho \sqbrk A = \openint \gets 0 \cup \openint 0 \to$
which by Union of Open Sets of Metric Space is Open is open.
Hence the result by definition of closed mapping.
== Sources ==
* : Part $\text {II}$: Counterexamples: $33$. Special Subsets of the Plane: $1$
Category:Real Number Plane with Euclidean Topology
Category:Closed Mappings
Projection onto Ideal of External Direct Sum of Rings

== Theorem ==
Let $\struct {R_1, +_1, \circ_1}, \struct {R_2, +_2, \circ_2}, \ldots, \struct {R_n, +_n, \circ_n}$ be rings.
Let $\ds \struct {R, +, \circ} = \prod_{k \mathop = 1}^n \struct {R_k, +_k, \circ_k}$ be their direct product.
For each $k \in \closedint 1 n$, let:
:${R_k}' = \set {\tuple {x_1, \ldots, x_n} \in R: \forall j \ne k: x_j = 0}$
Let $\pr_k: R \to {R_k}'$ be the projection on the $k$th coordinate of $\struct {R, +, \circ}$ onto ${R_k}'$.
Then $\pr_k$ is an epimorphism.
== Proof ==
From Ideal of External Direct Sum of Rings we already have that ${R_k}'$ is an ideal of $R$.
The result follows by application of Projection is Epimorphism.
== Also see ==
* Canonical Injection from Ideal of External Direct Sum of Rings
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $22$. New Rings from Old: Theorem $22.8$
* : $\S 3.1$: Direct sums
Category:Ideal Theory
Category:Projections
Projections on Direct Product of Group Homomorphisms

== Theorem ==
Let $G, H_1$ and $H_2$ be groups.
Let $H_1 \times H_2$ be the group direct product of $H_1$ and $H_2$.
Let $f_1: G \to H_1$ and $f_2: G \to H_2$ be group homomorphisms.
Let $f_1 \times f_2: g \to H_1 \times H_2$ be the direct product of $f_1$ and $f_2$.
Let:
:$\pr_1: H_1 \times H_2 \to H_1$ be the first projection from $H_1 \times H_2$ to $H_1$
:$\pr_2: H_1 \times H_2 \to H_2$ be the second projection from $H_1 \times H_2$ to $H_2$.
Then:
:$(1) \quad \pr_1 \circ \paren {f_1 \times f_2} = f_1$
:$(2) \quad \pr_2 \circ \paren {f_1 \times f_2} = f_2$
where $\circ$ is the operation of composition of mappings.
== Proof ==
The proof of $(2)$ follows exactly the same lines as the proof of $(1)$, so the proof of $(1)$ only will be shown here.
=== Matching Domains ===
From Domain of Composite Relation, the domain of $\pr_1 \circ \paren {f_1 \times f_2}$ is the domain of $f_1 \times f_2$.
By definition of the direct product of $f_1$ and $f_2$, the domain of $f_1 \times f_2$ is $G$.
Also by definition, the domain of $f_1$ is also $G$.
Thus the domains of $\pr_1 \circ \paren {f_1 \times f_2}$ and $f_1$ are the same. 
=== Matching Codomains ===
From Codomain of Composite Relation, the codomain of $\pr_1 \circ \paren {f_1 \times f_2}$ is the codomain of $\pr_1$.
By definition of the first projection $H_1 \times H_2$, the codomain of $\pr_1$ is $H_1$.
Also by definition, the codomain of $f_1$ is also $H_1$.
Thus the codomains of $\pr_1 \circ \paren {f_1 \times f_2}$ and $f_1$ are the same. 
=== Matching Images ===
Let $g \in G$.
Then:
So:
:$g \in G \implies \map {\pr_1 \circ \paren {f_1 \times f_2} } g = \map {f_1} g$
and so Equality of Mappings has been demonstrated.
== Sources ==
* : Chapter $\text{II}$: Groups: Direct Products
Category:Group Homomorphisms
Category:Group Direct Products
Projections on Direct Product of Normed Vector Spaces define Bounded Linear Transformations

== Theorem ==
Let $\Bbb F$ be a subfield of $\C$. 
Let $\struct {X, \norm {\, \cdot \,}_X}$ and $\struct {Y, \norm {\, \cdot \,}_Y}$ be normed vector spaces over $\Bbb F$.
Let $V = X \times Y$ be the direct product of the vector spaces $X$ and $Y$ together with induced component-wise operations.
Let $\norm {\, \cdot \,}_{X \times Y}$ be the direct product norm.
Define the maps $\Pi_X : X \times Y \to X$ and $\Pi_Y : X \times Y \to Y$ by: 
:$\map {\Pi_X} {x, y} = x$
and:
:$\map {\Pi_Y} {x, y} = y$ 
for all $x \in X$, $y \in Y$.
Then $\Pi_X$ and $\Pi_Y$ are bounded linear transformations.
== Proof ==
Let $\tuple {x_1, y_1}, \tuple {x_2, y_2} \in X \times Y$ and $\lambda \in \Bbb F$.
Then we have: 
and: 
So $\Pi_X$ and $\Pi_Y$ are linear. 
We now show that they are bounded.
Let $\tuple {x, y} \in X \times Y$.
Then:
and:
So $\Pi_X$ and $\Pi_Y$ are bounded.
Category:Direct Product of Vector Spaces
Projective Resolution Exists Iff Enough Projectives

== Theorem ==
Let $\AA$ be an abelian category.
Then $\AA$ has enough projectives any object in $\AA$ has a projective resolution.
== Proof ==
Suppose $\AA$ has enough projectives.
Let $X$ be an object in $\AA$.
Then there is an epimorphism $\varepsilon : P_0 \to X$ for some projective object $P_0$.
In particular
: $P_0 \to X \to 0$
is exact at $X$.
Since $\AA$ is abelian it has kernels.
Thus $\varepsilon$ has a kernel $K \to P_0$.
Since $\AA$ has enough projectives, there is an epimorphism $\tilde d_1 : P_1 \to K$.
Define $d_1 : P_1 \to K \to P_0$ by composition.
By Uniqueness of Epi-Mono Factorization and since this is an epi-mono factorization of $d_1$, $K$ is the image of $d_1$.
Hence
:$P_1 \to P_0 \to X \to 0$
is exact at $P_0$.
By induction there is a projective resolution of $X$.
Conversely suppose, that any object $X$ admits a projective resolution.
Then the augmentation map $\varepsilon: P_0 \to X$ is an epimorphism by a projective object $P_0$.
Hence $\AA$ has enough projectives.
Category:Homological Algebra
Projector has Norm 1

== Theorem ==
An idempotent operator $P$ is a projector on the Hilbert Space $H$ $P$ has norm $1$:
:$\ds \norm P \equiv \sup_{x \mathop \in H} \frac {\norm P} {\norm x} = 1$
== Proof ==
For all $x \in \Rng P$:
:$\norm {P \dfrac x {\norm x} } = \dfrac {\norm x} {\norm x} = 1$
so $\norm P \ge 1$.
It remains to show that this holds with equality $P$ is a projector.
First, suppose $P$ is a projector.
Let $\set {p_1, p_2, \ldots}$ be an orthonormal basis for $\Rng P$.
Let $\set {q_1, q_2, \ldots}$ be an orthonormal basis for $\Rng P_\perp$.
Then for any $x \in H$, we can choose scalars $\set {\alpha_1, \alpha_2, \ldots}$ and $\set {\beta_1, \beta_2, \ldots}$ so that:
:$\ds x = \sum_{i \mathop = 1}^\infty \alpha_i p_i + \sum_{i \mathop = 1}^\infty \beta_i q_i$
Because the basis vectors are orthogonal, Pythagoras's theorem shows that:
:$\ds \norm x^2 = \sum_{i \mathop = 1}^\infty \norm {\alpha_i}^2 + \norm {\beta_i}^2$
Then $\norm {P x}$ can be expanded thus:
Hence $\norm P \le 1$.
Since it was already shown $\norm P \ge 1$, it follows that $\norm P = 1$.
Now suppose $P$ is not a projector.
Then there exists $x \in H$ so that $P x - x$ is not orthogonal to $\Rng P$.
By writing $x = p + q$ with $p \in \Rng P$ and $q \in \Rng P_\perp$, it follows that:
:$P x - x = P \paren {p + q} - \paren {p + q} = P q - q$
By rescaling $x$, we can assume $\norm q = 1$.
Since $q \in \Rng P_\perp$ but
:$P q - q = P x - x = \notin \Rng P_\perp$
it follows that $P q \ne 0$.
Let $\norm {P q} = c \ne 0$.
It will be shown that
:$y = c q + \dfrac 1 c P q$
satisfies
:$\dfrac {\norm {P y} } {\norm y} > 1$
Notice first that:
Now:
Category:Hilbert Spaces
Proof by Cases

== Sequent ==
Proof by cases is a valid argument in types of logic dealing with disjunctions $\lor$.
This includes propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
=== Sequent Form ===
== Variants ==
The following forms can be used as variants of this theorem:
=== Formulation 1 ===
=== Formulation 2 ===
=== Formulation 3 ===
== Explanation ==
Thus a disjunction is eliminated from a sequent.
== Also known as ==
== Also see ==
* Definition:Disjunction
* Rule of Addition
* Principle of Dilemma
Category:Proof by Cases
Category:Conditional
Category:Disjunction
Category:Proof Techniques
Proof by Cases/Explanation

== Proof Rule ==
Proof by Cases can be expressed in natural language as follows:
We are given that either $\phi$ is true, or $\psi$ is true, or both.
Suppose we make the assumption that $\phi$ is true, and from that deduce that $\chi$ has to be true.
Then suppose we make the assumption that $\psi$ is true, and from that deduce that $\chi$ has to be true.
Therefore, it has to follow that the truth of $\chi$ follows from the fact of the truth of either $\phi$ or $\psi$.
Category:Proof by Cases
Proof by Cases/Formulation 1

== Theorem ==
: $\left({p \implies r}\right) \land \left({q \implies r}\right) \dashv \vdash \left({p \lor q}\right) \implies r$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof ==
Category:Proof by Cases
Proof by Cases/Formulation 1/Forward Implication

== Theorem ==
:$\paren {p \implies r} \land \paren {q \implies r} \vdash \paren {p \lor q} \implies r$
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction: Exercise $1 \ \text{(f)}$
* : $\S 1.13$: Tableau Problems (TAB1): CASES
Category:Proof by Cases
Proof by Cases/Formulation 1/Forward Implication/Proof 2

== Theorem ==
== Proof ==
From the Constructive Dilemma we have:
:$p \implies q, r \implies s \vdash p \lor r \implies q \lor s$
from which, changing the names of letters strategically:
:$p \implies r, q \implies r \vdash p \lor q \implies r \lor r$
From the Rule of Idempotence we have:
:$r \lor r \vdash r$
and the result follows by Hypothetical Syllogism.
Category:Proof by Cases
Proof by Cases/Formulation 1/Proof

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccccc||ccccc|} \hline
(p & \implies & r) & \land & (q & \implies & r) & (p & \lor & q) & \implies & r \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \F & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \F & \F & \T & \F & \F & \F & \T & \T & \F & \F \\
\F & \T & \T & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \T & \F & \F & \F \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \F & \F & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
Category:Truth Table Proofs
Category:Proof by Cases
Proof by Cases/Formulation 2

== Theorem ==
:$\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \iff \paren {\paren {p \lor q} \implies r}$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof ==
Category:Proof by Cases
Proof by Cases/Formulation 2/Forward Implication

== Theorem ==
:$\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \implies \paren {\paren {p \lor q} \implies r}$
== Proof 1 ==
== Proof by Truth Table ==
== Sources ==
* : $\S \text{II}$: Exercise $12 \ \text{(c)}$
Category:Proof by Cases
Proof by Cases/Formulation 2/Forward Implication/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
$\begin{array}{|ccccccc|c|ccccc|} \hline
((p & \implies & r) & \land & (q & \implies & r)) & \implies & ((p & \lor & q) & \implies & r) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \F & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \F & \F & \T & \F & \F & \T & \F & \T & \T & \F & \F \\
\F & \T & \T & \T & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \T & \T & \F & \F & \F \\
\T & \T & \T & \T & \F & \T & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \F & \F & \T & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
== Sources ==
* : $\S \text{II}$: Exercise $13$
Category:Proof by Cases
Category:Truth Table Proofs
Proof by Cases/Formulation 3

== Theorem ==
:$\vdash \paren {\paren {p \lor q} \land \paren {p \implies r} \land \paren {q \implies r} } \implies r$
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T49}$
Category:Proof by Cases
Proof by Cases/Proof Rule

== Proof Rule ==
Proof by cases is a valid argument in types of logic dealing with disjunctions $\lor$.
This includes propositional logic and predicate logic, and in particular natural deduction.
As a proof rule it is expressed in the form:
:If we can conclude $\phi \lor \psi$, and:
::$(1): \quad$ By making the assumption $\phi$, we can conclude $\chi$
::$(2): \quad$ By making the assumption $\psi$, we can conclude $\chi$
:then we may infer $\chi$.
The conclusion $\chi$ does not depend upon either assumption $\phi$ or $\psi$.
It can be written:
:$\ds {\phi \lor \psi \quad \begin{array}{|c|} \hline \phi \\ \vdots \\ \chi \\ \hline \end{array} \quad \begin{array}{|c|} \hline \psi \\ \vdots \\ \chi \\ \hline \end{array} \over \chi} \lor_e$
=== Tableau Form ===
== Explanation ==
== Also known as ==
== Also see ==
* This is a rule of inference of the following proof systems:
** Definition:Natural Deduction
== Technical Note ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction
* : $\S 1.2.1$: Rules for natural deduction
Category:Proof by Cases
Category:Rules of Inference
Proof by Cases/Proof Rule/Tableau Form

== Proof Rule ==
Let $\phi \lor \psi$ be a well-formed formula in a tableau proof whose main connective is the disjunction operator.
Let $\chi$ be a well-formed formula such that $\paren {\phi \vdash \chi}$, $\paren {\psi \vdash \chi}$.
Proof by Cases is invoked for $\phi \lor \psi$ as follows:
== Also defined as ==
Treatments that refer to this as the rule of or-elimination tend to use the abbreviation $\lor \EE$.
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction
Category:Tableau Proofs