avewright/proofwiki-math huggingface dataset:
Theorem: Impossible Proposition Strictly Implies Every Proposition

Let $P$ be a proposition of modal logic.
Let $P$ be not possibly true.
Then:
:$\forall Q: P \implies Q$
where $Q$ is an arbitrary proposition in the universe of discourse.

Proof:
{{ProofWanted|More background needed into Modal Logic}}
Theorem: Necessary Proposition is Strictly Implied by Every Proposition

Let $P$ be a proposition of modal logic.
Let $P$ be necessarily true.
Then:
:$\forall Q: Q \implies P$
where $Q$ is an arbitrary proposition in the universe of discourse.

Proof:
{{ProofWanted|More background needed into Modal Logic}}
Theorem: Impulse Imparted by Constant Force

Let a constant force $\mathbf F$ be applied to a particle $P$ from time $t_1$ to time $t_2$.
Then the impulse $\mathbf J$ imparted to $P$ is:
:$\mathbf J = \mathbf F \paren {t_2 - t_1}$

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf J
      | r = \int_{t_1}^{t_2} \mathbf F \rd t
      | c = {{Defof|Impulse}}
}}
{{eqn | r = \bigintlimits {\mathbf F t} {t \mathop = t_1} {t \mathop = t_2}
      | c = Definite Integral of Constant
}}
{{eqn | r = \mathbf F \paren {t_2 - t_1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Impulse equals Change in Momentum

Let a force $\mathbf F$ be applied to a particle $P$.
Then the impulse $\mathbf J$ imparted to $P$ is equal to the change of momentum of $P$.

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf F
      | r = \dfrac {\d \mathbf p} {\d t}
      | c = Newton's Second Law of Motion: $\mathbf p$ is the (linear) momentum of $P$
}}
{{eqn | ll= \leadsto
      | l = \int_{t_1}^{t_2} \mathbf F \rd t
      | r = \int_{t_1}^{t_2} \dfrac {\d \mathbf p} {\d t}
      | c = integrating $\mathbf F$ {{WRT|Integration}} time between limits $t_1$ to $t_2$
}}
{{eqn | ll= \leadsto
      | l = \mathbf J
      | r = \bigintlimits {\mathbf p} {t \mathop = t_1} {t \mathop = t_2}
      | c = {{Defof|Impulse}}, and Fundamental Theorem of Calculus
}}
{{eqn | r = \mathbf p_{t_2} - \mathbf p_{t_1}
      | c = 
}}
{{end-eqn}}
Hence the impulse $\mathbf J$ equals the change of (linear) momentum between $t_1$ and $t_2$, as required.
{{qed}}
Theorem: Category of Locales with Localic Mappings is Category

Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Then:
:$\mathbf{Loc_*}$ is a metacategory

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
For any two localic mappings their composition (in the usual set theoretic sense) is again a localic mapping by Composite Localic Mapping is Localic Mapping.
For any locale $L = \struct{S, \preceq}$, we have the identity mapping $\operatorname{id}_S$.
From Identity Mapping is Localic Mapping we have $\operatorname{id}_S$ is a localic mapping.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity, this is the identity morphism for $L$.
Finally by Composition of Mappings is Associative, the associative property is satisfied.
Hence $\mathbf{Loc_*}$ is a metacategory.
{{qed}}
Theorem: Composite Localic Mapping is Localic Mapping

Let $L_1 = \struct{S_1, \preceq_1}, L_2 = \struct{S_2, \preceq_2}$ and $L_3 = \struct{S_3, \preceq_3}$ be locales.
Let $f_1 : L_1 \to L_2$ and $f_2 : L_2 \to L_3$ be localic mappings.
Then:
:the composite $f_2 \circ f_1 : L_1 \to L_3$ is a localic mapping.

Proof:
By definition of a localic mapping:
:$f_1, f_2$ are the upper adjoint of Galois connections $\tuple{f_1, d_1}, \tuple{f_2, d_2}$ respectively
where $d_1 : L_2 \to L_1$ and $d_2 : L_3 \to L_2$ are frame homomorphsims.
From Composite Frame Homomorphism is Frame Homomorphism:
:$d_1 \circ d_2 : L_3 \to L_2$ is a frame homomorphsims
From Composition of Galois Connections is Galois Connection:
:$\tuple {f_2 \circ f_1, d_1 \circ d_2}$ is a Galois connection
Hence:
:$f_2 \circ f_1$ is the upper adjoint of a Galois connection
By definition of localic mapping:
:$f_2 \circ f_1$ is a localic mapping
{{qed}}
Theorem: Identity Mapping is Localic Mapping

Let $L = \struct {S, \preceq}$ be a locale.
Let $\operatorname{id}_S : S \to S$ be the identity mapping on $S$.
Then:
:$\operatorname{id}_S : L \to L$ is a localic mapping.

Proof:
By definition of localic mapping, we need to show that $\operatorname{id}_S$ is the upper adjoint of a Galois connection where  the lower adjoint is a frame homomorphism of $L$ to $L$.
From Identity Mapping forms Galois Connection:
:$\tuple{\operatorname{id}_S, \operatorname{id}_S}$ is a Galois connection
From Identity Mapping is Frame Homomorphism
:$\operatorname{id}_S$ is a frame homomorphism of $L$ to $L$
The result follows.
{{qed}}
Theorem: Category of Locales with Localic Mappings is Isomorphic to Category of Locales

Let $\mathbf{Loc}$ denote the category of locales.
Let $\mathbf{Loc_*}$ denote the category of locales with localic mappings.
Then:
:$\mathbf{Loc_*}$ is isomorphic to $\mathbf{Loc}$
with isomorphisms:
:$F : \mathbf{Loc} \to \mathbf{Loc_*}$ defined by:
::for each locale $L$ of $\mathbf{Loc} : \map F L = L$
::for each continuous map $f : L_1 \to L_2$ of $\mathbf{Loc} : \map F f = f_*$
:where:
::$f^* : L_2 \to L_1$ denotes frame homomorphism such that $f = \paren{f^*}^{\operatorname{op}}$
::$f_* : L_1 \to L_2$ denotes the upper adjoint of the frame homomorphism $f^* : L_2 \to L_1$
and
:$G : \mathbf{Loc_*} \to \mathbf{Loc}$ be defined by:
::for each locale $L$ of $\mathbf{Loc_*} : \map G L = L$
::for each localic mapping $g : L_1 \to L_2$ of $\mathbf{Loc_*} : \map G g = \paren{g^*}^{\operatorname{op}}$
:where:
::$g^* : L_2 \to L_1$ denotes the frame homomorphism that is the lower adjoint of the localic mapping $g$
::$\paren{g^*}^{\operatorname{op}}$ denotes the opposite morphism of the frame homomorphism

Proof:
By definitions of category of locales and category of locales with localic mappings:
:the objects of $\mathbf{Loc}$ and $\mathbf{Loc_*}$ are locales
:the morphisms of $\mathbf{Loc}$ are continuous maps
:the morphisms of $\mathbf{Loc_*}$ are localic mappings
By definition of continuous maps:
:$f : L_1 \to L_2$ is a continuous map {{iff}} there exists a frame homomorphism $f^* : L_2 \to L_1 :$
::$f = \paren{f^*}^{\operatorname{op}}$
By definition of localic mapping:
:$g : L_1 \to L_2$ is a localic mapping {{iff}} there exists a frame homomorphism $g^* : L_2 \to L_1 :$
::$\tuple{g, g^*}$ is a Galois connection
Theorem: Category of Locales with Localic Mappings is Isomorphic to Category of Locales/Lemma 1

:$F : \mathbf{Loc} \to \mathbf{Loc_*}$ is a well-defined covariant functor

Proof:
=== $F$ is Well-defined ===
By definition of $\mathbf{Loc}$ and $\mathbf {Loc_*}$ the objects of $\mathbf{Loc}$ are the objects of $\mathbf{Loc_*}$.
The object functor of $F$ is the identity object functor and so is well-defined.
Let $f : L_1 \to L_2$ be a continuous map of $\mathbf{Loc}$.
By definition of continuous map:
:there exists a frame homomorphism $\loweradjoint f : L_2 \to L_1$ such that $f = \paren{\loweradjoint f}^{\operatorname{op}}$.
From Frame Homomorphism is Lower Adjoint of Galois Connection:
:there exists an upper adjoint $\upperadjoint f$ such that $\tuple{\upperadjoint f, \loweradjoint f}$ is a Galois connection.
From Galois Connection is Unique for Given Lower Adjoint, it follows that $\loweradjoint f$ is unique.
Hence the morphism functor of $F$ is well-defined.
{{qed|lemma}}
Theorem: Category of Locales with Localic Mappings is Isomorphic to Category of Locales/Lemma 2

:$G : \mathbf{Loc_*} \to \mathbf{Loc}$ is a well-defined covariant functor

Proof:
=== $G$ is Well-defined ===
By definition of $\mathbf{Loc_*}$ and $\mathbf {Loc}$ the objects of $\mathbf{Loc_*}$ are the objects of $\mathbf{Loc}$.
The object functor of $G$ is the identity object functor and so is well-defined.
Let $g : L_1 \to L_2$ be a localic mapping of $\mathbf{Loc_*}$.
By definition of localic mapping:
:there exists a Galois connection $\tuple{\upperadjoint g, \loweradjoint g}$ such that $g = \upperadjoint g$ and $\loweradjoint g$ is a frame homomorphism.
From Galois Connection is Unique for Given Upper Adjoint, it follows that the Galois connection $\tuple{\upperadjoint g, \loweradjoint g}$ is unique.
By definition of dual category:
:$\paren{\loweradjoint g}^{\operatorname{op}}$ is a morphism of $\mathbf {Loc}$.
Hence the morphism functor of $G$ is well-defined.
{{qed|lemma}}
Theorem: Category of Locales with Localic Mappings is Isomorphic to Category of Locales/Lemma 3

:$GF = \operatorname{id}_{\mathbf {Loc}}$

Proof:
By definition of $\mathbf{Loc}$ and $\mathbf {Loc_*}$ the objects of $\mathbf{Loc}$ are the objects of $\mathbf{Loc_*}$.
The object functors of $F$ and $G$ are the identity object functor and so $GF$ is the identity object functor.
Let $f : L_1 \to L_2$ be a continuous map of $\mathbf{Loc}$.
By definition of continuous map:
:there exists a frame homomorphism $\loweradjoint f : L_2 \to L_1$ such that $f = \paren{\loweradjoint f}^{\operatorname{op}}$.
From Frame Homomorphism is Lower Adjoint of Galois Connection:
:there exists an upper adjoint $\upperadjoint f$ such that $\tuple{\upperadjoint f, \loweradjoint f}$ is a Galois connection.
We have:
{{begin-eqn}}
{{eqn | l = GF f
      | r = \map G {Ff}
      | c = {{Defof|Composition of Functors}}
}}
{{eqn | r = \map G {\upperadjoint f}
      | c = definition of $F$
}}
{{eqn | r = \paren{\loweradjoint f}^{\operatorname{op} }
      | c = definition of $G$
}}
{{eqn | r = f
      | c = {{Defof|Continuous Map (Locale)|Continuous Map}}
}}
{{end-eqn}}
Hence $GF$ is the identity morphism functor.
The result follows.
{{qed}}
Category:Category of Locales with Localic Mappings is Isomorphic to Category of Locales
otipdfkx71xcs2a3l554hrefpwtkxl3
Theorem: Category of Locales with Localic Mappings is Isomorphic to Category of Locales/Lemma 4

:$FG = \operatorname{id}_{\mathbf {Loc_*}}$

Proof:
By definition of $\mathbf{Loc_*}$ and $\mathbf {Loc}$ the objects of $\mathbf{Loc_*}$ are the objects of $\mathbf{Loc}$.
The object functors of $G$ and $F$ are the identity object functor and so $FG$ is the identity object functor.
Let $g : L_1 \to L_2$ be a localic mapping of $\mathbf{Loc_*}$.
By definition of localic mapping:
:there exists a Galois connection $\tuple{\upperadjoint g, \loweradjoint g}$ such that $g = \upperadjoint g$ and $\loweradjoint g$ is a frame homomorphism.
We have:
{{begin-eqn}}
{{eqn | l = FG g
      | r = \map F {Gg}
      | c = {{Defof|Composition of Functors}}
}}
{{eqn | r = \map F {\paren{\loweradjoint g}^{\operatorname{op} } }
      | c = definition of $G$
}}
{{eqn | r = \upperadjoint g
      | c = definition of $F$
}}
{{eqn | r = g
      | c = {{Defof|Localic Mapping}}
}}
{{end-eqn}}
Hence $FG$ is the identity morphism functor.
The result follows.
{{qed}}
Category:Category of Locales with Localic Mappings is Isomorphic to Category of Locales
f85010v8kw3n6xazdgmkwmugldqdvw4
Theorem: Cube of n minus 23 Greater than Square of (4n-7)

Let $n \in \Z$ such that $n \ge 12$.
Then:
:$n^3 - 23 > \paren {4 n - 7}^2$

Proof:
The proof proceeds by induction.
For all $n \in \Z$ such that $n \ge 12$, let $\map P n$ be the proposition:
:$n^3 - 23 > \paren {4 n - 7}^2$
Theorem: Point with Zero Second Derivative is not necessarily Point of Inflection

Let $f$ be a real function which is twice differentiable on the open interval $\openint a b$.
Let
:$\map {f' '} \xi = 0$
where $\map {f' '} \xi$ denotes the second derivative of $f$ at $\xi \in \openint a b$.
Then it is not necessarily the case that $f$ has a point of inflection at $\xi$.

Proof:
Consider the function:
:$f: \R \to \R: \forall x \in \R: \map f x = x^4$
This has a local minimum at $x = 0$ at which $\map {f' '} x = 0$.
But $x = 0$ is not a point of inflection of $f$.
{{qed}}
Theorem: Information Contained in Letter of Alphabet

Let $\psi$ be a letter of the English alphabet.
To a first degree of approximation, the quantity of information contained in $\psi$ is $4 \cdotp 7$.
That is, there is approximately $4 \cdotp 7$ times as much information conveyed by transmission of a single letter as a single bit.

Proof:
Let it be assumed for the purposes of this exercise that each letter has an equal probability of occurring as an element of a message.
There are $26$ letters of the English alphabet.
The amount of information contained in $\psi$ is therefore:
:$\map I \psi = \dfrac {\lg 26} {\lg 2} \approx 4 \cdotp 7$
where $\lg$ denotes the binary logarithm.
{{qed}}
{{MissingLinks|the rule that gives $\dfrac {\lg 26} {\lg 2}$}}
Theorem: Floor Function/Examples/Floor of 4.35

:$\floor {4 \cdotp 35} = 4$

Proof:
We have that:
:$4 \le 4 \cdotp 35 < 5$
Hence $4$ is the floor of $4 \cdotp 35$ by definition.
{{qed}}
Theorem: Ceiling Function/Examples/Ceiling of 4.35

:$\ceiling {4 \cdotp 35} = 5$

Proof:
We have that:
:$4 < 4 \cdotp 35 \le 5$
Hence $5$ is the ceiling of $4 \cdotp 35$ by definition.
{{qed}}
Theorem: Primitives which Differ by Constant/Corollary

Let $f$ be an integrable function on the closed interval $\closedint a b$.
Then there exist an uncountable number of primitives for $f$ on $\closedint a b$.

Proof:
By definition of integrable function, $f$ has a primitive $F$ (at least one).
By Primitives which Differ by Constant, for every real number $C$, if $\map F x$ is a primitive of $f$, then so is $\map G x$ where:
:$\forall x \in \closedint a b: \map G x = \map F x + c$
The Real Numbers are Uncountable.
Hence the result.
{{qed}}
Category:Primitives which Differ by Constant
ntadqkyzeok08l2w39kbjenms8sbk13
Theorem: Position of Interpolated Point under Linear Interpolation

Let $f$ be a real function.
Let $y_1, y_2, \ldots, y_n$ be known values of $f$ corresponding to $x_1, x_2, \ldots, x_n$ respectively.
Let $x'$ be in the domain of $f$ such that $x_i < x' < x_{i + 1}$.
Let $y' = \map f {x'}$ be determined according to linear interpolation.
Then:
:$y' = y_i + \dfrac {\paren {x' - x_i} \paren {y_{i + 1} - y_i} } {x_{i + 1} - x_i}$

Proof:
By definition of linear interpolation, the three points $\tuple {x_i, y_i}$, $\tuple {x', y'}$ and $\tuple {x_{i + 1}, y_{i + 1} }$ are all collinear.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {y' - y_i} {x' - x_i}
      | r = \dfrac {y_{i + 1} - y_i} {x_{i + 1} - x_i}
      | c = Two-Point Form of Equation of Straight Line in Plane
}}
{{eqn | ll= \leadsto
      | l = y' - y_i
      | r = \dfrac {\paren {x' - x_i} \paren {y_{i + 1} - y_i} } {x_{i + 1} - x_i}
      | c = multiplying both sides by $x' - x_i$
}}
{{eqn | ll= \leadsto
      | l = y'
      | r = y_i + \dfrac {\paren {x' - x_i} \paren {y_{i + 1} - y_i} } {x_{i + 1} - x_i}
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Catenary/Whewell

The '''catenary''' can be described by the Whewell equation:
:$s = a \tan \psi$
where:
:$s$ is the arc length
:$\psi$ is the turning angle
:$a$ is a constant.

Proof:
By definition, the '''catenary''' is the shape made by an ideally flexible chain hanging freely from two arbitrary points.
Let the '''catenary''' $\CC$ lie in a Cartesian plane.
Let the lowest point on $\CC$ be $P_0$.
Let $P$ be an arbitrary point on the chain.
Let $s$ be the length along the arc of the chain from the $P_0$ to $P$.
Let $w$ be the linear mass density of the chain, that is, its weight per unit length.
The section of chain between the lowest point and $P$ is in static equilibrium under the influence of three forces, as follows:
:The tension $T_0$ at $P_0$
:The tension $T$ at $P$
:The weight $w s$ of the chain between these two points.
As the chain is (ideally) flexible, the tension $T$ is along the line of the chain, and therefore along a tangent to the chain.
At $P_0$, the tangent to $\CC$ is a horizontal line.
Let the angle between the tangent to $\CC$ at $P$ and that (horizontal) tangent to $\CC$ at $P_0$ be $\psi$.
By definition, $\psi$ is the turning angle of $\CC$.
{{handwaving|I believe a mathematical justification of this statement is incomplete. Needs attention and consideration as to exactly what "turning angle" is. We are trying to capture the idea that it's the rate of change of angle with respect to distance travelled. Hence this argument needs more careful thought.}}
:520px
Let us resolve $T$ into its horizontal and vertical components:
:$T_0 = T \cos \psi$
:$w s = T \sin \psi$
We divide one by the other to eliminate $T$ and set $a = T_0 / w$:
:$\tan \psi = \dfrac s a$
from which the result follows.
{{qed}}
Theorem: Image of Element under Inverse Mapping/Corollary 2

:$\forall y \in T: \map f {\map {f^{-1} } y} = y$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S, y \in T
      | l = \map f x
      | r = y
      | c = 
}}
{{eqn | lo= \iff
      | l = \map {f^{-1} } y
      | r = x
      | c = Image of Element under Inverse Mapping
}}
{{eqn | q = \forall y \in T
      | ll= \leadsto
      | l = \map f {\map {f^{-1} } y}
      | r = y
      | c = substituting $\map {f^{-1} } y$ for $x$
}}
{{end-eqn}}
{{qed}}
Theorem: Image of Element under Inverse Mapping/Corollary 1

:$\forall x \in S: \map {f^{-1} } {\map f x} = x$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S, y \in T
      | l = \map f x
      | r = y
      | c = 
}}
{{eqn | lo= \iff
      | l = \map {f^{-1} } y
      | r = x
      | c = Image of Element under Inverse Mapping
}}
{{eqn | q = \forall x \in S
      | ll= \leadsto
      | l = \map {f^{-1} } {\map f x}
      | r = x
      | c = substituting $\map f x$ for $y$
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse of Strictly Monotone Continuous Real Function is Strictly Monotone and Continuous

Let $f$ be a continuous real function which is defined on the closed interval $I := \closedint a b$.
Let $f$ be strictly monotone on $I$.
Then $f$ has an inverse function $f^{-1}$ which is continuous and strictly monotone on $f \sqbrk I$.

Proof:
The function $f$ is a bijection from Strictly Monotone Real Function is Bijective.
From Inverse of Strictly Monotone Function, $f^{-1}$ is strictly monotone on  on $f \sqbrk I$.
From Continuous Real Function on Closed Interval is Bijective iff Strictly Monotone, $f^{-1}$ is a continuous real function.
Hence the result.
{{qed}}
Theorem: Area under Arc of Sine Function

:$\ds \int_0^\pi \sin x \rd x = 2$

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^\pi \sin x \rd x
      | r = \bigintlimits {-\cos x} 0 \pi
      | c = Primitive of Sine Function
}}
{{eqn | r = 2
      | c = Cosine of $\pi$, {{cos|0}}
}}
{{end-eqn}}
{{qed}}
Category:Sine Function
Category:Definite Integrals involving Sine Function
scun1ir668xgx0evll4r7ss32kk3bvw
Theorem: Matroid Rank Function Iff Matroid Rank Axioms

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Then:
:$\rho$ is the rank function of a matroid $M = \struct{S, \mathscr I}$.
{{iff}}:
:$\rho$ satisfies the rank axioms

Proof:
Follows immediately from:
:* Formulation 1 Rank Axioms Implies Rank Function of Matroid
:* Rank Function of Matroid Satisfies Formulation 1 Rank Axioms
Theorem: Principle of Open Induction for Real Numbers

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 of all such $x$.
By Set Difference is Subset:
:$T \subseteq \closedint a b$
so by Subset of Bounded Below Set is Bounded Below:
:$T$ is bounded below.
Since $T$ is non-empty by assumption, it follows from the Greatest Lower Bound Property that:
:$T$ admits an infimum.
Let $x_0 := \inf T$ be the infimum of $T$.
By definition, $x_0$ is a lower bound of $T$.
Therefore:
:$\forall x \in \closedint a b: x < x_0 \implies x \in S$
or equivalently:
:$\hointr a {x_0} \subseteq S$
Hence, {{hypothesis}}:
:$x_0 \in S$
By definition of open set, there exists some $\epsilon > 0$ such that:
:$\openint {x_0 - \epsilon} {x_0 + \epsilon} \subseteq S$
By Union of Subsets is Subset:
:$\hointr a {x_0} \cup \openint {x_0 - \epsilon} {x_0 + \epsilon} = \hointr a {x_0 + \epsilon} \subseteq S$
Thus, by Set Difference with Subset is Superset of Set Difference:
:$T = \paren {\closedint a b \setminus S} \subseteq \paren {\closedint a b \setminus \hointr a {x_0 + \epsilon}} = \closedint {x_0 + \epsilon} b$
Therefore, $x_0 + \epsilon$ is a lower bound of $T$.
Hence, by definition of infimum, it must hold that:
:$x_0 + \epsilon \le x_0$
But that implies that:
:$\epsilon \le 0$
contradicting the definition of $\epsilon$.
We are forced to conclude that our assumption:
:$\exists x \in \closedint a b \setminus S$
was incorrect.
Therefore, by Proof by Contradiction:
:$\closedint a b \subseteq S$
{{qed}}
Theorem: Equivalence of Definitions of Matroid Rank Axioms/Formulation 2 Implies Formulation 1

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 2 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 2}}
Then $\rho$ satisfies formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}

Proof:
==== $\rho$ satisfies $(\text R 1)$ ====
We have:
{{begin-eqn}}
{{eqn | l = 0
      | o = \le 
      | r = \map \rho \O
      | c = Rank axiom $(\text R 4)$
}}
{{eqn | o = \le 
      | r = \card \O
      | c = Rank axiom $(\text R 4)$
}}
{{eqn | r = 0
      | c = Cardinality of Empty Set
}}
{{end-eqn}}
Hence:
:$\map \rho \O = 0$
{{qed|lemma}}
==== $\rho$ satisfies $(\text R 2)$ ====
Let $X \subseteq S$.
Let $y \in S$.
We have:
{{begin-eqn}}
{{eqn | l = \map \rho X
      | o = \le
      | r = \map \rho {X \cup y}
      | c = Rank axiom $(\text R 5)$
}}
{{eqn | o = \le
      | r = \map \rho X + \map \rho {\set y} - \map \rho {X \cup \set y}
      | c = Rank axiom $(\text R 6)$
}}
{{eqn | o = \le
      | r = \map \rho X + \map \rho {\set y}
}}
{{eqn | o = \le
      | r = \map \rho X + \card {\set y}
      | c = Rank axiom $(\text R 4)$
}}
{{eqn | o = \le
      | r = \map \rho X + 1
      | c = Cardinality of Singleton
}}
{{end-eqn}}
This proves rank axiom $(\text R 2)$
{{qed|lemma}}
==== $\rho$ satisfies $(\text R 3)$ ====
Let $X \subseteq S$.
Let $x, y \in S$.
Let $\map \rho {X \cup \set x} = \map \rho {X \cup \set y} = \map \rho X$.
We have:
{{begin-eqn}}
{{eqn | l = \map \rho X
      | o = \le
      | r = \map \rho {X \cup \set x \cup \set y }
      | c = Rank axiom $(\text R 5)$
}}
{{eqn | r = \map \rho {\paren{X \cup \set x} \cup  \paren{X \cup \set y} }
}}
{{eqn | o = \le
      | r = \map \rho {X \cup \set x} + \map \rho {X \cup \set x} - \map \rho {\paren{X \cup \set x} \cap  \paren{X \cup \set y} }
      | c = Rank axiom $(\text R 6)$
}}
{{eqn | o = \le
      | r = \map \rho {X \cup \set x} + \map \rho {X \cup \set x} - \map \rho X
}}
{{eqn | r = \map \rho X + \map \rho X - \map \rho X
}}
{{eqn | r = \map \rho X
}}
{{end-eqn}}
Hence:
:$\map \rho {X \cup \set x \cup \set y} = \map \rho X$
This proves rank axiom $(\text R 3)$
Theorem: Equivalence of Definitions of Matroid Rank Axioms/Formulation 1 Implies Formulation 2

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Then $\rho$ satisfies formulation 2 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 2}}

Proof:
Follows immediately from:
:* Formulation 1 Rank Axioms Implies Rank Function of Matroid
:* Rank Function of Matroid Satisfies Formulation 2 Rank Axioms