nyuuzyou/wikis huggingface dataset:
Double Angle Formulas/Hyperbolic Sine/Corollary

== Corollary to Double Angle Formula for Hyperbolic Sine ==
: $\map \sinh {2 \theta} = \dfrac {2 \tanh \theta} {1 - \tanh^2 \theta}$
where $\sinh$ and $\tanh$ denote hyperbolic sine and hyperbolic tangent respectively.
== Proof ==
Category:Hyperbolic Sine Function
Category:Hyperbolic Tangent Function
Category:Double Angle Formula for Hyperbolic Sine
Double Angle Formulas/Hyperbolic Tangent

== Theorem ==
: $\tanh 2 x = \dfrac {2 \tanh x} {1 + \tanh^2 x}$
where $\tanh$ denotes hyperbolic tangent.
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
== Sources ==
* : $\S 8$: Hyperbolic Functions: $8.26$: Double Angle Formulas
Category:Hyperbolic Tangent Function
Category:Double Angle Formula for Hyperbolic Tangent
Double Angle Formulas/Sine

== Theorem ==
:$\sin 2 \theta = 2 \sin \theta \cos \theta$
where $\sin$ and $\cos$ denote sine and cosine respectively.
=== Corollary ===
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
== Proof 4 ==
== Also see ==
* Double Angle Formula for Cosine
== Sources ==
* : $\text V$. Trigonometry: Formulae $(16)$
* : $\S 5$: Trigonometric Functions: $5.38$
* : $\S 16.3 \ (3) \ \text{(iii)}$
* 
* 
* 
* 
* : Appendix $12$: Trigonometric formulae: Double-angle formulae
* : Appendix $14$: Trigonometric formulae: Double-angle formulae
Category:Double Angle Formula for Sine
Category:Double Angle Formulas
Category:Sine Function
Double Angle Formulas/Sine/Proof 3

== Theorem ==
== Proof ==
Consider an isosceles triangle $\triangle ABC$ with base $BC$ and apex $\angle BAC = 2 \alpha$.
Construct the angle bisector to $\angle BAC$ and name it $AH$:
:$\angle BAH = \angle CAH = \alpha$
From Bisector of Apex of Isosceles Triangle is Perpendicular to Base:
:$AH \perp BC$
From Area of Triangle in Terms of Two Sides and Angle:
By definition of sine:
and so:
Category:Double Angle Formula for Sine
Double Angle Formulas/Tangent

== Theorem ==
:$\tan 2 \theta = \dfrac {2 \tan \theta} {1 - \tan^2 \theta}$
where $\tan$ denotes tangent.
=== Corollary ===
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
== Sources ==
* : $\text V$. Trigonometry: Formulae $(19)$
* : $\S 5$: Trigonometric Functions: $5.40$
* 
* 
* 
* : Appendix $12$: Trigonometric formulae: Double-angle formulae
* : Appendix $14$: Trigonometric formulae: Double-angle formulae
Category:Double Angle Formula for Tangent
Category:Double Angle Formulas
Category:Tangent Function
Double Centralizer Generated by Element of C*-Algebra is Double Centralizer

== Theorem ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $c \in A$.
Define $L_c : A \to A$ and $R_c : A \to A$ by:
:$\map {L_c} a = c a$
and:
:$\map {R_c} a = a c$
for each $a \in A$. 
Then $\tuple {L_c, R_c}$ is a double centralizer of $A$. 
== Proof ==
First, for each $a \in A$ we have:
:$\norm {\map {L_c} a} \le \norm c \norm a$
and:
:$\norm {\map {R_c} a} \le \norm a \norm c$
by the definition of an algebra norm.
Now, for $a, b \in A$ we have:
and:
Finally, we have:
Hence $\tuple {L_c, R_c}$ is a double centralizer of $A$.
== Sources ==
* : $2.1$: $\text C^\ast$-Algebras
Category:Multiplier Algebras
Double Induction Principle

== Theorem ==
Let $M$ be a class.
Let $g: M \to M$ be a mapping on $M$.
Let $M$ be a minimally inductive class under $g$.
Let $\RR$ be a relation on $M$ which satisfies:
Then $\map \RR {x, y}$ holds for all $x, y \in M$.
=== Minimally Closed Class ===
The Double Induction Principle can be made more general by applying it to a minimally closed class:
=== General Derivation ===
== Proof 1 ==
== Proof 2 ==
== Also known as ==
The Double Induction Principle can also be referred to as the Principle of Double Induction.
Some authors refer to this principle by its initials: D.I.P.
== Also see ==
* Double Superinduction Principle
Category:Mathematical Induction
Category:Named Theorems
Category:Proof Techniques
Category:Minimally Closed Classes
Category:Double Induction Principle
Double Induction Principle/General

== Theorem ==
Let $M$ be a class.
Let $g: M \to M$ be a mapping on $M$.
Let $M$ be a minimally inductive class under $g$.
Let $\RR$ be a relation which satisfies the following conditions:
Then:
:$\forall x, y \in M: \map \RR {x, y}$
== Proof ==
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 9$ Supplement -- optional: Theorem $S_1$
Category:Double Induction Principle
Category:General Double Induction Principle
Double Induction Principle/Lemma

== Lemma for Double Induction Principle ==
Let $M$ be a minimally inductive class under a mapping $g$.
Let $\RR$ be a relation on $M$ which satisfies:
Let $x$ be a right normal element of $M$ with respect to $\RR$.
Then $x$ is also a left normal element of $M$ with respect to $\RR$.
== Proof ==
The proof proceeds by general induction.
Let $x \in M$ be right normal with respect to $\RR$.
Let $\map P y$ be the proposition:
:$\map \RR {x, y}$ holds.
=== Basis for the Induction ===
By condition $\text D_1$ of the definition of $\RR$:
:$\map \RR {x, \O}$
for all $x \in M$.
Thus $\map P \O$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P y$ is true, where $x \in M$, then it logically follows that $\map P {\map g y}$ is true.
So this is the induction hypothesis:
:$\map \RR {x, y}$ holds
from which it is to be shown that:
:$\map \RR {x, \map g y}$ holds.
=== Induction Step ===
This is the induction step:
Let $\map \RR {x, y}$ hold.
As $x$ is right normal with respect to $\RR$:
:$\map \RR {y, x}$ holds.
Thus by condition $\text D_2$ of the definition of $\RR$:
:$\map \RR {x, \map g y}$ holds.
So $\map P x \implies \map P {\map g x}$ and the result follows by the Principle of General Induction.
Therefore:
:$\forall x \in M$: if $x$ is a right normal element of $M$ with respect to $\RR$, then $x$ is a left normal element of $M$ with respect to $\RR$
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 4$ A double induction principle and its applications: Theorem $4.3$
Category:Double Induction Principle
Double Induction Principle/Minimally Closed Class

== Theorem ==
Let $M$ be a class which is closed under a progressing mapping $g$.
Let $b$ be an element of $M$ such that $M$ is minimally closed under $g$ with respect to $b$.
Let $\RR$ be a relation on $M$ which satisfies:
Then $\map \RR {x, y}$ holds for all $x, y \in M$.
== Proof ==
The proof proceeds by general induction.
Let an element $x$ of $M$ be defined as:
:left normal with respect to $\RR$ $\map \RR {x, y}$ for all $y \in M$
:right normal with respect to $\RR$ $\map \RR {y, x}$ for all $y \in M$.
Let the hypothesis be assumed.
First we demonstrate a lemma:
=== Lemma ===
We now show by general induction that every $x \in M$ is right normal with respect to $\RR$.
It then follows from the lemma that $\map \RR {x, y}$ for all $x, y \in M$.
=== Basis for the Induction ===
$\map P b$ is the case:
From condition $\text D_1$ of the definition of $\RR$, we have immediately that:
:$\map \RR {x, b}$
for all $x \in M$.
That is, that $b$ is right normal with respect to $\RR$.
Thus $\map P b$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P x$ is true, where $x \in M$, then it logically follows that $\map P {\map g x}$ is true.
So this is the induction hypothesis:
:$x$ is right normal with respect to $\RR$
from which it is to be shown that:
:$\map g x$ is right normal with respect to $\RR$.
=== Induction Step ===
This is the induction step:
Let $x \in M$ be right normal with respect to $\RR$:
:$\forall y \in M: \map \RR {y, x}$
By the lemma we have that $x$ is left normal with respect to $\RR$.
That is:
:$\forall y \in M: \map \RR {x, y}$
Thus by condition $\text D_2$ of the definition of $\RR$:
:$\forall y \in M: \map \RR {y, \map g x}$
That is, $\map g x$ is right normal with respect to $\RR$.
So $\map P x \implies \map P {\map g x}$ and by the Principle of General Induction for Minimally Closed Class:
:$\forall x \in M$: $x$ is right normal with respect to $\RR$.
The result follows.
Category:Double Induction Principle
Double Induction Principle/Minimally Closed Class/Lemma

== Theorem ==
Let $M$ be a class which is closed under a progressing mapping $g$.
Let $b$ be an element of $M$ such that $M$ is minimally closed under $g$ with respect to $b$.
Let $\RR$ be a relation on $M$ which satisfies:
Let $x$ be a right normal element of $M$ with respect to $\RR$.
Then $x$ is also a left normal element of $M$ with respect to $\RR$.
== Proof ==
The proof proceeds by general induction.
Let $x \in M$ be right normal with respect to $\RR$
Let $\map P y$ be the proposition:
:$\map \RR {x, y}$ holds.
=== Basis for the Induction ===
By condition $\text D_1$ of the definition of $\RR$:
:$\map \RR {x, b}$
for all $x \in M$.
Thus $\map P \O$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P y$ is true, where $x \in M$, then it logically follows that $\map P {\map g y}$ is true.
So this is the induction hypothesis:
:$\map \RR {x, y}$ holds
from which it is to be shown that:
:$\map \RR {x, \map g y}$ holds
=== Induction Step ===
This is the induction step:
Let $\map \RR {x, y}$ hold.
As $x$ is right normal with respect to $\RR$:
:$\map \RR {y, x}$ holds.
Thus by condition $\text D_2$ of the definition of $\RR$:
:$\map \RR {x, \map g y}$ holds.
So $\map P x \implies \map P {\map g x}$ and the result follows by the Principle of General Induction.
Therefore:
:$\forall x \in M$: if $x$ is a right normal element of $M$ with respect to $\RR$, then $x$ is a left normal element of $M$ with respect to $\RR$
Category:Double Induction Principle
Double Induction Principle/Proof 1

== Theorem ==
== Proof ==
The proof proceeds by general induction.
Let an element $x$ of $M$ be defined as:
:left normal with respect to $\RR$ $\map \RR {x, y}$ for all $y \in M$
:right normal with respect to $\RR$ $\map \RR {y, x}$ for all $y \in M$.
Let the hypothesis be assumed.
First we demonstrate a lemma:
=== Lemma ===
We now show by general induction that every $x \in M$ is right normal with respect to $\RR$.
It then follows from the lemma that $\map \RR {x, y}$ for all $x, y \in M$.
=== Basis for the Induction ===
$\map P \O$ is the case:
From condition $\text D_1$ of the definition of $\RR$, we have immediately that:
:$\map \RR {x, \O}$
for all $x \in M$.
That is, that $\O$ is right normal with respect to $\RR$.
Thus $\map P \O$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P x$ is true, where $x \in M$, then it logically follows that $\map P {\map g x}$ is true.
So this is the induction hypothesis:
:$x$ is right normal with respect to $\RR$
from which it is to be shown that:
:$\map g x$ is right normal with respect to $\RR$.
=== Induction Step ===
This is the induction step:
Let $x \in M$ be right normal with respect to $\RR$:
:$\forall y \in M: \map \RR {y, x}$
By the lemma we have that $x$ is left normal with respect to $\RR$.
That is:
:$\forall y \in M: \map \RR {x, y}$
Thus by condition $\text D_2$ of the definition of $\RR$:
:$\forall y \in M: \map \RR {y, \map g x}$
That is, $\map g x$ is right normal with respect to $\RR$.
So $\map P x \implies \map P {\map g x}$ and by the Principle of General Induction:
:$\forall x \in M$: $x$ is right normal with respect to $\RR$.
The result follows.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 4$ A double induction principle and its applications: Theorem $4.3$
Category:Double Induction Principle
Double Induction Principle/Proof 2

== Theorem ==
== Proof ==
By definition, a minimally inductive class under $g$ is a minimally closed class under $g$ with respect to $\O$.
Recall the Double Induction Principle for Minimally Closed Class:
Let $\RR$ be a relation on $M$ which satisfies:
Then $\map \RR {x, y}$ holds for all $x, y \in M$.
In this context:
:$b = \O$
and the result follows.
Category:Double Induction Principle
Double Negation

== Theorem ==
== Double Negation Introduction ==
== Double Negation Elimination ==
== Combined Double Negation Law ==
These are often combined into one law:
=== Formulation 1 ===
=== Formulation 2 ===
== Intuitionist Perspective ==
== Also see ==
* Definition:Logical Not
* Double Negation Elimination implies Law of Excluded Middle
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 3$
* : Chapter $1$: The Propositional Calculus $1$: $2$ Conditionals and Negation
* : $\S 3$: Statements and conditions; quantifiers
* : Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic
* 
* : $\S 1.2.1$: Rules for natural deduction
* 
Category:Double Negation
Category:Logical Negation
Double Negation/Double Negation Elimination

== Theorem ==
The rule of double negation elimination is a valid argument in certain types of logic dealing with negation $\neg$.
This includes classical propositional logic and predicate logic, and in particular natural deduction, but for example not intuitionistic propositional logic.
=== Proof Rule ===
=== Sequent Form ===
== Intuitionist Perspective ==
== Also see ==
* Definition:Logical Not
* Double Negation Elimination implies Law of Excluded Middle
== Sources ==
* : $\S 2.3$: Basic Truth-Tables of the Propositional Calculus
Category:Double Negation Elimination
Category:Double Negation
Double Negation/Double Negation Elimination/Proof Rule

== Theorem ==
The rule of double negation elimination is a valid argument in certain types of logic dealing with negation $\neg$.
This includes classical propositional logic and predicate logic, and in particular natural deduction, but for example not intuitionistic propositional logic.
As a proof rule it is expressed in the form:
:If we can conclude $\neg \neg \phi$, then we may infer $\phi$.
It can be written:
:$\ds {\neg \neg \phi \over \phi} \neg \neg_e$
=== Tableau Form ===
== Intuitionist Perspective ==
== Also see ==
* This is a rule of inference of the following proof systems:
** Definition:Natural Deduction
== Technical Note ==
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 3$
* : $\S 1.2.1$: Rules for natural deduction
Category:Rules of Inference
Category:Double Negation Elimination
Double Negation/Double Negation Elimination/Proof Rule/Technical Note

== Technical Note on ==
When invoking in a tableau proof, use the template:
:{{DoubleNegElimination|line|pool|statement|depends}}
or:
:{{DoubleNegElimination|line|pool|statement|depends|comment}}
where:
:line is the number of the line on the tableau proof where is to be invoked
:pool is the pool of assumptions (comma-separated list)
:statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
:depends is the line of the tableau proof upon which this line directly depends
:comment is the (optional) comment that is to be displayed in the Notes column.
Category:Technical Notes
Double Negation/Double Negation Elimination/Sequent Form/Formulation 1/Proof

== Theorem ==
== Proof ==
== Intuitionist Perspective ==
== Also see ==
* Double Negation Elimination implies Law of Excluded Middle
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $2$ Conditionals and Negation
Category:Double Negation Elimination
Double Negation/Double Negation Elimination/Sequent Form/Formulation 2

== Theorem ==
:$\vdash \neg \neg p \implies p$
== Proof ==
== Intuitionist Perspective ==
== Also see ==
* Double Negation Elimination implies Law of Excluded Middle
== Sources ==
* : $\S 4.7$: The Derivation of Formulae: $D \, 16$
* : $\text{I}$: 'NOT' and 'IF': $\S 5$: Theorem $\text{T11}$
* : Chapter $2$: The Propositional Calculus $2$: $2$: Theorems and Derived Rules: Theorem $40$
Category:Double Negation Elimination
Double Negation/Double Negation Introduction/Proof Rule

== Proof Rule ==
The rule of double negation introduction is a valid argument in types of logic dealing with negation $\neg$.
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$, then we may infer $\neg \neg \phi$.
It can be written:
:$\ds {\phi \over \neg \neg \phi} \neg \neg_i$
=== Tableau Form ===
== Also see ==
* This is a rule of inference of the following proof systems:
** Definition:Natural Deduction
* Double Negation Elimination: Proof Rule
== Technical Note ==
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 3$
* : $\S 1.2.1$: Rules for natural deduction
Category:Rules of Inference
Category:Double Negation Introduction
Double Negation/Double Negation Introduction/Proof Rule/Technical Note

== Proof Rule on ==
When invoking in a tableau proof, use the template:
:{{DoubleNegIntro|line|pool|statement|depends}}
or:
:{{DoubleNegIntro|line|pool|statement|depends|comment}}
where:
:line is the number of the line on the tableau proof where is to be invoked
:pool is the pool of assumptions (comma-separated list)
:statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
:depends is the line of the tableau proof upon which this line directly depends
:comment is the (optional) comment that is to be displayed in the Notes column.
Category:Technical Notes
Double Negation/Double Negation Introduction/Sequent Form/Formulation 2

== Theorem ==
:$\vdash p \implies \neg \neg p$
== Proof ==
== Sources ==
* : $\S 4.7$: The Derivation of Formulae: $D \, 15$
* : $\text{I}$: 'NOT' and 'IF': $\S 5$: Theorem $\text{T12}$
* : Chapter $2$: The Propositional Calculus $2$: $2$: Theorems and Derived Rules: Theorem $39$
Category:Double Negation Introduction
Double Negation/Formulation 1/Proof 2

== Theorem ==
== Proof ==
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, appropriate truth values match for both boolean interpretations.
$\quad \begin{array}{|c||ccc|} \hline
p & \neg & \neg & p \\
\hline
\F & \F & \T & \F \\
\T & \T & \F & \T \\
\hline
\end{array}$
Hence:
:$p \dashv \vdash \neg \neg p$
== Intuitionist Perspective ==
Category:Double Negation
Category:Truth Table Proofs
Double Negation/Formulation 2

== Theorem ==
:$\vdash p \iff \neg \neg p$
== Proof 1 ==
== Proof by Truth Table ==
== Intuitionist Perspective ==
== Sources ==
* : $\S 3.6$: Reference Formulae: $RF \, 7$
* : $\S 4.7$: The Derivation of Formulae: $D \, 17$
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T110}$
* : $3$: The Method of Deduction: $3.2$: The Rule of Replacement: $14.$
* : $\S \text{II}$: The Logic of Statements $(2): \ 6$: Using logical equivalences: $14$
* : $\S 1$: Informal statement calculus: $\S 1.2$: Truth functions and truth tables: Example $1.6 \ \text{(c)}$
* : $\S 1.14$: Exercise $12 \ (1)$
Category:Double Negation
Double Negation/Formulation 2/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.
$\quad \begin{array}{|c|c|ccc|} \hline
p & \iff & \neg & \neg & p \\
\hline
\F & \T & \F & \T & \F \\
\T & \T & \T & \F & \T \\
\hline
\end{array}$
== Intuitionist Perspective ==
== Sources ==
* : $\S \text{II}$: Exercise $14 \ \text{(a)}$
* : $2$ Arguments Containing Compound Statements: $2.4$: Statement Forms
Category:Double Negation
Double Negation/Intuitionist Perspective

== Double Negation: Intuitionistic Perspective ==
The intuitionist school rejects the Law of the Excluded Middle as a valid logical axiom.
This in turn invalidates the Law of Double Negation Elimination from the system of intuitionistic propositional logic.
Hence a difference is perceived between Double Negation Elimination and Double Negation Introduction, whereby it can be seen from the Principle of Non-Contradiction that if a statement is true, then it is not the case that it is false.
However, if all we know is that a statement is not false, we can not be certain that it is actually true without accepting that there are only two possible truth values.
Such distinctions may be important when considering, for example, multi-value logic.
However, when analysing logic from a purely classical standpoint, it is common and acceptable to make the simplification of taking just one Double Negation rule:
:$p \dashv \vdash \neg \neg p$
== Sources ==
* 
* 
Category:Law of Excluded Middle
Double Negation Elimination implies Law of Excluded Middle

== Theorem ==
Let the Law of Double Negation Elimination be supposed to hold:
:$\neg \neg p \vdash p$
Then the Law of Excluded Middle likewise holds:
:$\vdash p \lor \neg p$
== Proof 1 ==
== Proof 2 ==
== Intuitionist Perspective ==
Category:Double Negation Elimination implies Law of Excluded Middle
Category:Double Negation Elimination
Category:Double Negation
Double Negation Elimination implies Law of Excluded Middle/Proof 1

== Theorem ==
== Proof ==
== Intuitionist Perspective ==
== Sources ==
* : Chapter $2$: The Propositional Calculus $2$: $2$: Theorems and Derived Rules: Theorem $44$
* : $\S 1.2.2$: Derived rules
Category:Double Negation Elimination implies Law of Excluded Middle
Double Negation with Erroneous Conjunction

== Source Work ==
:
: Chapter $1$: Informal statement calculus
::$1.2$. Truth functions and truth tables: Example $1.6 \ \text{(c)}$
== Mistake ==
:$\paren {p \leftrightarrow \paren {\land \paren {\sim p} } }$ is a tautology.
== Correction ==
As it stands, this statement is meaningless, as $\land$ is a binary operator.
The most obvious assumption is that $\land$ is a typo for $\sim$, and that:
:$\paren {p \leftrightarrow \paren {\sim \paren {\sim p} } }$ is a tautology.
is meant.
See Double Negation/Formulation 2 for an analysis of this.
Note that in :
:$\sim$ is the symbol used for $\neg$, the logical negation operator
:$\leftrightarrow$ is the symbol used for $\iff$, the biconditional operator.
== Sources ==
* : $\S 1$: Informal statement calculus: $\S 1.2$: Truth functions and truth tables: Example $1.6 \ \text{(c)}$
Category:Mistakes/Logic for Mathematicians
Double Orthocomplement is Closed Linear Span

== Theorem ==
Let $H$ be a Hilbert space.
Let $A \subseteq H$ be a subset of $H$.
Then the following identity holds:
:$\paren {A^\perp}^\perp = \vee A$
Here $A^\perp$ denotes orthocomplementation, and $\vee A$ denotes the closed linear span.
=== Corollary ===
== Proof ==
From Orthocomplement is Closed Linear Subspace:
:$\paren {A^\perp}^\perp$ is a closed linear subspace of $H$.
Also:
:$\paren {A^\perp}^\perp \supseteq A$
Indeed, for each $a \in A$, we have:
:$\forall a' \in A^\perp : \innerprod a {a'} = 0$
by definition of $A^\perp$.
This also means that:
:$a \in \paren{A^\perp}^\perp$
by definition of $\paren{A^\perp}^\perp$.
Hence:
:$\vee A \subseteq \paren{A^\perp}^\perp$
For the converse direction, note:
:$A \subseteq \vee A$
Now apply Orthocomplement Reverses Subset twice:
:$\paren {A^\perp}^\perp \subseteq \paren {\paren {\vee A}^\perp}^\perp$
By Double Orthocomplement of Closed Linear Subspace:
:$\paren{A^\perp}^\perp \subseteq \vee A$
== Sources ==
* : $\text{I}$ Hilbert Spaces: $\S 2.$ Orthogonality: Corollary $2.10$
Category:Hilbert Spaces
Category:Orthocomplements
Double Orthocomplement is Closed Linear Span/Corollary

== Corollary to Double Orthocomplement is Closed Linear Span ==
Let $H$ be a Hilbert space.
Let $A \subseteq H$ be a closed linear subspace of $H$.
Then:
:$\paren {A^\perp}^\perp = A$
== Proof ==
Since $A$ is a subspace of $H$, it is closed under linear combination, so: 
:$\map \span A = A$
We therefore have:
while from Double Orthocomplement is Closed Linear Span, we have: 
:$\paren {A^\perp}^\perp = \vee A$
So, we obtain: 
:$\paren {A^\perp}^\perp = A$
== Sources ==
* : $\text{I}$ Hilbert Spaces: $\S 2.$ Orthogonality: Corollary $2.9$
Category:Hilbert Spaces