avewright/proofwiki-math huggingface dataset:
Theorem: Openness Relation on Topological Spaces is Transitive

Let $T_1 = \struct {S_1, \tau_1}$ be a topological space
Let $S_2 \subseteq S_1$ be a subset of $S_1$.
Let $S_3 \subseteq S_2$ be a subset of $S_2$.
Let $T_2 = \struct {S_2, \tau_2}$ be the topological subspace of $T_1$ such that $\tau_2$ is the subspace topology induced by $\tau_1$.
Let $T_3 = \struct {S_3, \tau_3}$ be the topological subspace of $T_2$ such that $\tau_3$ is the subspace topology induced by $\tau_2$.
Let:
:$S_2$ be an open set of $T_1$
:$S_3$ be an open set of $T_2$.
Then:
:$S_3$ is an open set of $T_1$.

Proof:
We have by definition of subspace topology that:
:$\tau_2 = \set {U \cap S_2: U \in \tau_1}$
Then we have {{hypothesis}} that:
:$S_3 \in \tau_2$
and so:
:$S_3 \in \set {U \cap S_2: U \in \tau_1}$
That is, $S_3$ is the intersection of $U$ and $S_2$, both of which are open sets of $T_1$.
Hence by {{Open-set-axiom|2}}, $S_3$ is an open set of $T_1$.
{{qed}}
Theorem: Induced Topology on Subspace of Subspace Coincides with Induced Topology on Subspace

Let $T_1 = \struct {S_1, \tau_1}$ be a topological space
Let $S_2 \subseteq S_1$ be a subset of $S_1$.
Let $S_3 \subseteq S_2$ be a subset of $S_2$.
Let $T_2 = \struct {S_2, \tau_2}$ be the topological subspace of $T_1$ such that $\tau_2$ is the subspace topology on $T_2$ induced by $\tau_1$.
Let $T_3 = \struct {S_3, \tau_3}$ be the topological subspace of $T_1$ such that $\tau_3$ is the subspace topology on $T_3$ induced by $\tau_1$.
Then $\tau_3$ is the same set of subsets of $S_1$ as is the subspace topology on $T_3$ induced by $\tau_2$.

Proof:
Let $\tau_P$ denote the subspace topology on $T_3$ induced by $\tau_1$.
Let $\tau_Q$ denote the subspace topology on $T_3$ induced by $\tau_2$.
The object of this exercise is to demonstrate that $\tau_P = \tau_Q$.
This will be done by showing that an arbitrary set $V$ is in $\tau_P$ {{iff}} $V$ is in $\tau_Q$.
We have that:
:$\tau_P = \set {U \cap S_3: U \in \tau_1}$
:$\tau_Q = \set {U \cap S_3: U \in \tau_2}$
Then:
{{begin-eqn}}
{{eqn | l = V
      | o = \in
      | r = \tau_P
      | c = 
}}
{{eqn | q = \exists U_1 \in \tau_1
      | l = V
      | r = U_1 \cap S_3
      | c = 
}}
{{eqn | r = U_1 \cap \paren {S_2 \cap S_3}
      | c = Intersection with Subset is Subset
}}
{{eqn | r = \paren {U_1 \cap S_2} \cap S_3
      | c = Intersection is Associative
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists U_2 \in \tau_2
      | l = V
      | r = U_2 \cap S_3
      | c = {{Defof|Subspace Topology}}: $U_1 \cap S_2 \in \tau_2$
}}
{{eqn | ll= \leadstoandfrom
      | l = V
      | o = \in
      | r = \tau_Q
      | c = Definition of $\tau_Q$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Real-Valued Function on Finite Set is Bounded

Let $S$ be a finite set.
Let $f: S \to \R$ be a real-valued function on $S$.
Then $f$ is bounded.

Proof:
Let $K$ be defined as:
:$K = \ds \max_{x \mathop \in S} \size {\map f x}$
where $\size {\map f x}$ denotes the absolute value of $\map f x$.
Then trivially:
:$\exists K \in \R_{\ge 0}: \forall x \in S: \size {\map f x} \le K$
This is the definition of a bounded real-valued function.
{{qed}}
Theorem: Reciprocal Function is Continuous on Real Numbers without Zero

Let $\R_{\ne 0}$ denote the real numbers excluding $0$:
:$\R_{\ne 0} := \R \setminus \set 0$.
Let $f: \R_{\ne 0} \to \R$ denote the reciprocal function:
:$\forall x \in \R_{\ne 0}: \map f x = \dfrac 1 x$
Then $f$ is continuous on all real intervals which do not include $0$.

Proof:
From Identity Mapping is Continuous, the real function $g$ defined as:
:$\forall x \in \R: \map g x = x$
is continuous on $\R$.
From Constant Mapping is Continuous, the real function $h$ defined as:
:$\forall x \in \R: \map x h = 1$
We note that $\map g 0 = 0$.
The result then follows from Quotient Rule for Continuous Real Functions:
:$\map f x = \dfrac {\map h x} {\map g x}$
is continuous wherever $\map g x \ne 0$.
{{qed}}
Category:Reciprocals
Category:Examples of Continuous Real Functions
qxrww5v46h8fic2h55de5gtnkcbmw0m
Theorem: Reciprocal Function is Unbounded on Open Unit Interval

Let $A = \openint 0 1$ denote the open unit interval.
Let $f: A \to \R$ be the reciprocal function:
:$\forall x \in A: \map f x := \dfrac 1 x$
Then $f$ is unbounded.

Proof:
Let $K \in \R_{>0}$.
Then:
:$\exists x \in \R: 0 < x < \dfrac 1 K$ such that $x < 1$.
Then we have:
:$\map f x = \dfrac 1 x > K$
So whatever $K$ may be, it can never be large enough to be a bound of $f$ on $\openint 0 1$.
{{qed}}
Theorem: Continuous Real-Valued Function is not necessarily Bounded

Let $S$ be a set.
Let $f: S \to \R$ be a continuous real-valued function.
Then $f$ is not necessarily bounded.

Proof:
Let $S$ denote the (open) real interval $\openint 0 1$.
Let $f: S \to \R$ denote the reciprocal function:
:$\forall x \in S: \map f x = \dfrac 1 x$
From Reciprocal Function is Continuous on Real Numbers without Zero, $f$ is continuous on $S$.
From Reciprocal Function is Unbounded on Open Unit Interval, $f$ is unbounded on $S$.
Hence the result, by Proof by Counterexample.
{{qed}}
Theorem: Set of Inverse Positive Integers with Zero is Compact

Let $K$ be the set of inverse positive integers with zero:
:$\ds K := \set {1, \frac 1 2, \frac 1 3, \dots} \cup \set 0$
Let $\struct {\R, \size {\, \cdot \,}}$ be the normed vector space of real numbers.
Then $K$ is compact in real numbers.

Proof:
We have that $K \subset \closedint 0 1$.
Hence, $K$ is bounded.
Furthermore:
:$\ds \R \setminus K = \openint {-\infty} 0 \cup \paren {\bigcup_{n \mathop = 1}^\infty \openint {\frac 1 {n + 1}} {\frac 1 n}} \cup \openint 1 \infty$
By Union of Open Sets of Normed Vector Space is Open, $\R \setminus K$ is open.
By definition, $K$ is closed.
By Heine-Borel theorem, $K$ is compact.
{{qed}}
Theorem: Space of Continuous on Closed Interval Real-Valued Functions with Pointwise Addition and Pointwise Scalar Multiplication forms Vector Space

Let $I := \closedint a b$ be a closed real interval.
Let $\map C I$ be the space of real-valued functions continuous on $I$.
Let $\struct {\R, +_\R, \times_\R}$ be the field of real numbers.
Let $\paren +$ be the pointwise addition of real-valued functions.
Let $\paren {\, \cdot \,}$ be the pointwise scalar multiplication of real-valued functions.
Then $\struct {\map C I, +, \, \cdot \,}_\R$ is a vector space.

Proof:
Let $f, g, h \in \map C I$ such that:
:$f, g, h : I \to \R$
Let $\lambda, \mu \in \R$.
Let $\map 0 x$ be a real-valued function such that:
:$\map 0 x : I \to 0$.
Let us use real number addition and multiplication.
$\forall x \in I$ define pointwise addition as:
:$\map {\paren {f + g}} x := \map f x +_\R \map g x$.
Define pointwise scalar multiplication as:
:$\map {\paren {\lambda \cdot f}} x := \lambda \times_\R \map f x$
Let $\map {\paren {-f} } x := -\map f x$.
Theorem: Space of Continuously Differentiable on Closed Interval Real-Valued Functions with Pointwise Addition and Pointwise Scalar Multiplication forms Vector Space

Let $I := \closedint a b$ be a closed real interval.
Let $\map C I$ be a space of real-valued functions continuous on $I$.
Let $\map {C^1} I$ be a space of continuously differentiable functions on $I$.
Let $\struct {\R, +_\R, \times_\R}$ be the field of real numbers.
Let $\paren +$ be the pointwise addition of real-valued functions.
Let $\paren {\, \cdot \,}$ be the pointwise scalar multiplication of real-valued functions.
Then $\struct {\map {C^1} I, +, \, \cdot \,}_\R$ is a vector space.

Proof:
From Space of Continuous on Closed Interval Real-Valued Functions with Pointwise Addition and Pointwise Scalar Multiplication forms Vector Space:
:$\struct {\map C I, +, \, \cdot \,}_\R$ is a vector space.
By Differentiable Function is Continuous:
:$\map {C^1} I \subset \map C I$
Let $f, g \in \map {C^1} I$.
Let $\alpha \in \R$.
Let $\map 0 x$ be a real-valued function such that:
:$\map 0 x : I \to 0$
Restrict $\paren +$ to $\map {C^1} I \times \map {C^1} I$.
Restrict $\paren {\, \cdot \,}$ to $\R \times \map {C^1} I$.
Theorem: P-Sequence Space with Pointwise Addition and Pointwise Scalar Multiplication on Ring of Sequences forms Vector Space

Let $\ell^p$ be the p-sequence space.
Let $\struct {\R, +_\R, \times_\R}$ be the field of real numbers.
Let $\paren +$ be the pointwise addition on the ring of sequences.
Let $\paren {\, \cdot \,}$ be the pointwise multiplication on the ring of sequences.
Then $\struct {\ell^p, +, \, \cdot \,}_\R$ is a vector space.

Proof:
Let $\sequence {a_n}_{n \mathop \in \N}, \sequence {b_n}_{n \mathop \in \N}, \sequence {c_n}_{n \mathop \in \N} \in \ell^p$.
Let $\lambda, \mu \in \R$.
Let $\sequence 0 := \tuple {0, 0, 0, \dots}$ be a real-valued function.
Let us use real number addition and multiplication.
Define pointwise addition as:
:$\sequence {a_n + b_n}_{n \mathop \in \N} := \sequence {a_n}_{n \mathop \in \N} +_\R \sequence {b_n}_{n \mathop \in \N}$.
Define pointwise scalar multiplication as:
:$\sequence {\lambda \cdot a_n}_{n \mathop \in \N} := \lambda \times_\R \sequence {a_n}_{n \mathop \in \N}$
Let the additive inverse be $\sequence {-a_n} := - \sequence {a_n}$.
Theorem: Vector Space of Continuous on Closed Interval Real Functions is not Finite Dimensional

Let $I := \closedint 0 1$ be a closed real interval.
Let $\struct {\map C I, +, \, \cdot \,}_\R$ be the continuous on closed interval real function vector space.
Then $\struct {\map C I, +, \, \cdot \,}_\R$ is not finite dimensional.

Proof:
=== Monomials are linearly independent ===
Let $d \in \N_{>0}$.
Consider the set of real monomials of the following form:
:$\map {x_n} t = t^n$
where $n \in \N_{>0}$ and $n \le d$.
{{AimForCont}} the set of $x_n$ is not linearly independent.
Then:
:$\forall n \in \N_{>0}: n \le d: \exists \alpha_n \in \R: \neg \forall n: \alpha_n \ne 0$
and:
:$\ds \sum_{k \mathop = 1}^d \alpha_k t^k = 0$
Let $m \in \N_{>0}: m \le d$ be the smallest index such that $\alpha_m \ne 0$.
Then:
:$\ds \forall t \in \closedint 0 1: \sum_{k \mathop = m}^d \alpha_k t^k = 0$
or
:$\ds \forall t \in \hointl 0 1: \sum_{k \mathop = m}^d \alpha_k t^{k - d} = 0$
Note that:
:$\ds \forall n \in \N_{>0}: \exists t \in \hointl 0 1: t = \frac 1 n$
Thus:
:$\ds \forall n \in \N_{>0}: \sum_{k \mathop = m}^d \frac {\alpha_k} {n^{d - k} } = 0$
Passing the limit $n \to \infty$ gives us $\alpha_d = 0$.
This is a contradiction.
Hence, the set of $x_n$ is linearly independent.
{{qed|lemma}}
Theorem: Min Operation Equals an Operand

Let $x_1, x_2, \dotsc, x_n \in S$ for some $n \in \N_{>0}$.
Then:
:$\exists i \in \closedint 1 n : x_i = \min \set {x_1, x_2, \dotsc, x_n}$

Proof:
We will prove the result by induction on the number of operands $n$.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\exists i \in \closedint 1 n : x_i = \min \set {x_1, x_2, \dotsc, x_n}$
Theorem: Min Operation Yields Infimum of Parameters/General Case

Let $x_1, x_2, \dots ,x_n \in S$ for some $n \in \N_{>0}$.
Then:
:$\min \set {x_1, x_2, \dotsc, x_n} = \inf \set {x_1, x_2, \dotsc, x_n}$

Proof:
We will prove the result by induction on the number of operands $n$.
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$\min \set {x_1, x_2, \dotsc, x_n} = \inf \set {x_1, x_2, \dotsc, x_n}$
Theorem: Primitive of Reciprocal of Root of a x squared plus b x plus c/a greater than 0

Let $a \in \R_{> 0}$.
Then for $x \in \R$ such that $a x^2 + b x + c > 0$:
:<nowiki>$\ds \int \frac {\d x} {\sqrt {a x^2 + b x + c} } = \begin {cases}
\dfrac 1 {\sqrt a} \ln \size {2 \sqrt a \sqrt {a x^2 + b x + c} + 2 a x + b} + C & : b^2 - 4 a c > 0 \\ \\
\dfrac 1 {\sqrt a} \map \arsinh {\dfrac {2 a x + b} {\sqrt {4 a c - b^2} } } + C & : b^2 - 4 a c < 0 \\ \\
\dfrac 1 {\sqrt a} \ln \size {2 a x + b} + C & : b^2 - 4 a c = 0
\end {cases}$</nowiki>
where $\arsinh$ denotes the area hyperbolic sine function.

Proof:
=== Completing the Square ===
{{:Primitive of Reciprocal of Root of a x squared plus b x plus c/a greater than 0/Completing the Square}}
Theorem: Primitive of Reciprocal of Root of a x squared plus b x plus c/a less than 0

Let $a \in \R_{< 0}$.
Then for $x \in \R$ such that $a x^2 + b x + c > 0$:
:$\ds \int \frac {\d x} {\sqrt {a x^2 + b x + c} } = \dfrac {-1} {\sqrt {-a} } \map \arcsin {\dfrac {2 a x + b} {\sqrt {\size {b^2 - 4 a c} } } } + C$
given that $b^2 \ne 4 a c$.

Proof:
=== Completing the Square ===
{{:Primitive of Reciprocal of Root of a x squared plus b x plus c/a less than 0/Completing the Square}}
Theorem: Primitive of Reciprocal of Root of a x squared plus b x plus c/a greater than 0/Negative Discriminant

Let $a \in \R_{>0}$.
Let $b^2 - 4 a c < 0$.
Then for $x \in \R$ such that $a x^2 + b x + c > 0$:
:$\ds \int \frac {\d x} {\sqrt {a x^2 + b x + c} } = \frac 1 {\sqrt a} \map \arsinh {\dfrac {2 a x + b} {\sqrt {4 a c - b^2} } } + C$
where $\arsinh$ denotes the area hyperbolic sine function.

Proof:
Let $b^2 - 4 a c < 0$.
Then:
{{begin-eqn}}
{{eqn | l = - D
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -D
      | r = q^2
      | c = for some $q \in \R$
}}
{{eqn | ll= \leadsto
      | l = q
      | r = \sqrt {4 a c - b^2}
      | c = by definition of $D$
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sqrt{a x^2 + b x + c} }
      | r = \frac 1 {\sqrt a} \int \frac {\d z} {\sqrt {z^2 + q^2} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 {\sqrt a} \map \arsinh {\frac z q} + C
      | c = Primitive of $\dfrac 1 {\sqrt {x^2 + a^2} }$
}}
{{eqn | r = \frac 1 {\sqrt a} \map \arsinh {\frac {2 a x + b} {\sqrt {4 a c - b^2} } } + C
      | c = substituting for $z$ and $q$
}}
{{end-eqn}}
Theorem: Primitive of Reciprocal of Root of a x squared plus b x plus c/a greater than 0/Positive Discriminant

Let $a, b, c \in \R$ such that $a > 0$.
Let $b^2 - 4 a c > 0$.
Then for $x \in \R$ such that $a x^2 + b x + c > 0$:
:$\ds \int \frac {\d x} {\sqrt {a x^2 + b x + c} } = \dfrac 1 {\sqrt a} \ln \size {2 \sqrt a \sqrt {a x^2 + b x + c} + 2 a x + b} + C$

Proof:
Let $b^2 - 4 a c > 0$.
Then:
{{begin-eqn}}
{{eqn | l = D
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = D
      | r = q^2
      | c = for some $q \in \R$
}}
{{eqn | ll= \leadsto
      | l = q
      | r = \sqrt {b^2 - 4 a c}
      | c = by definition of $D$
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sqrt {a x^2 + b x + c} }
      | r = \frac 1 {\sqrt a} \int \frac {\d z} {\sqrt {z^2 - q^2} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 {\sqrt a} \ln \size {z + \sqrt {z^2 - q^2} } + C
      | c = Primitive of $\dfrac 1 {\sqrt {x^2 - a^2} }$
}}
{{eqn | r = \frac 1 {\sqrt a} \ln \size {2 a x + b + \sqrt {\paren {2 a x + b}^2 - \paren {b^2 - 4 a c} } } + C
      | c = substituting for $z$ and $q$
}}
{{eqn | r = \frac 1 {\sqrt a} \ln \size {2 a x + b + \sqrt {4 a \paren {a x^2 + b x + c} } } + C
      | c = Completing the Square
}}
{{eqn | r = \frac 1 {\sqrt a} \ln \size {2 \sqrt a \sqrt {a x^2 + b x + c} + 2 a x + b} + C
      | c = rearranging
}}
{{end-eqn}}
Theorem: Primitive of Reciprocal of Root of a x squared plus b x plus c/a less than 0/Positive Discriminant

Let $a \in \R_{<0}$.
Let $b^2 - 4 a c > 0$.
Then for $x \in \R$ such that $a x^2 + b x + c > 0$ and $\size {2 a x + b} < \sqrt {b^2 - 4 a c}$:
:$\ds \int \frac {\d x} {\sqrt {a x^2 + b x + c} } = \frac {-1} {\sqrt {-a} } \map \arcsin {\frac {2 a x + b} {\sqrt {b^2 - 4 a c} } } + C$

Proof:
Let $b^2 - 4 a c > 0$.
Then:
{{begin-eqn}}
{{eqn | l = D
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = D
      | r = q^2
      | c = for some $q \in \R$
}}
{{eqn | ll= \leadsto
      | l = q
      | r = \sqrt {b^2 - 4 a c}
      | c = by definition of $D$
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sqrt {a x^2 + b x + c} }
      | r = \frac {-1} {\sqrt {-a} } \int \frac {\d z} {\sqrt {q^2 - z^2} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac {-1} {\sqrt {-a} } \arcsin \frac z q + C
      | c = Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$
}}
{{eqn | r = \frac {-1} {\sqrt {-a} } \map \arcsin {\frac {2 a x + b} {\sqrt {b^2 - 4 a c} } } + C
      | c = substituting for $z$ and $q$
}}
{{end-eqn}}
Theorem: Primitive of Reciprocal of Root of a x squared plus b x plus c/a less than 0/Negative Discriminant

Let $a \in \R_{> 0}$.
Let $b^2 - 4 a c > 0$.
Then for $x \in \R$ such that $a x^2 + b x + c > 0$:
:$\ds \int \frac {\d x} {\sqrt {a x^2 + b x + c} } = \frac {-1} {\sqrt {-a} } \map \arcsin {\frac {2 a x + b} {\sqrt {4 a c - b^2} } } + C$

Proof:
Let $b^2 - 4 a c < 0$.
Let $D' = -D = 4 a c - b^2$.
Then:
{{begin-eqn}}
{{eqn | l = D'
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = D
      | r = q^2
      | c = for some $q \in \R$
}}
{{eqn | ll= \leadsto
      | l = q
      | r = \sqrt {4 a c - b^2}
      | c = by definition of $D$
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sqrt {a x^2 + b x + c} }
      | r = \frac {-1} {\sqrt {-a} } \int \frac {\d z} {\sqrt {D - z^2} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac {-1} {\sqrt {-a} } \int \frac {\d z} {\sqrt {-D' - z^2} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac {-1} {\sqrt {-a} } \int \frac {\d z} {\sqrt {q^2 - z^2} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac {-1} {\sqrt {-a} } \arcsin \frac z q + C
      | c = Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$
}}
{{eqn | r = \frac {-1} {\sqrt {-a} } \map \arcsin {\frac {2 a x + b} {\sqrt {4 a c - b^2} } } + C
      | c = substituting for $z$ and $q$
}}
{{end-eqn}}
Theorem: Primitive of Reciprocal of Root of a x squared plus b x plus c/a greater than 0/Zero Discriminant

Let $a \in \R_{>0}$.
Let $b^2 - 4 a c = 0$.
Then for $x \in \R$ such that $a x^2 + b x + c > 0$:
:$\ds \int \frac {\d x} {\sqrt {a x^2 + b x + c} } = \frac 1 {\sqrt a} \ln \size {2 a x + b} + C$

Proof:
Let $b^2 - 4 a c = 0$ {{hypothesis}}.
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sqrt {a x^2 + b x + c} }
      | r = \int \frac {2 \sqrt a \rd x} {\sqrt {\paren {2 a x + b}^2} }
      | c = from $(1)$
}}
{{eqn | r = 2 \sqrt a \int \frac {\d x} {2 a x + b}
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = 2 \sqrt a \frac 1 {2 a} \ln \size {2 a x + b} + C
      | c = Primitive of $\dfrac 1 {a x + b}$
}}
{{eqn | r = \frac 1 {\sqrt a} \ln \size {2 a x + b} + C
      | c = simplifying
}}
{{end-eqn}}
Theorem: Primitive of Reciprocal of Root of a x squared plus b x plus c/a less than 0/Zero Discriminant

Let $a \in \R_{\ne 0}$.
Let $b^2 - 4 a c = 0$.
Then:
:$\ds \int \frac {\d x} {\sqrt {a x^2 + b x + c} }$
is not defined.

Proof:
Suppose that $b^2 - 4 a c = 0$.
Then:
{{begin-eqn}}
{{eqn | l = a x^2 + b x + c
      | r = \frac {\paren {2 a x + b}^2 - \paren {b^2 - 4 a c} } {4 a}
      | c = Completing the Square
}}
{{eqn | r = \frac {\paren {2 a x + b}^2} {4 a}
      | c = as $b^2 - 4 a c = 0$
}}
{{end-eqn}}
But we have that:
:$\paren {2 a x + b}^2 > 0$
while under our assertion that $a < 0$:
:$4 a < 0$
and so:
:$a x^2 + b x + c < 0$
Thus on the real numbers $\sqrt {a x^2 + b x + c}$ is not defined.
Hence it follows that:
:$\ds \int \frac {\d x} {\sqrt {a x^2 + b x + c} }$
is not defined.
Theorem: Space of Somewhere Differentiable Continuous Functions on Closed Interval is Meager in Space of Continuous Functions on Closed Interval

Let $I = \closedint a b$. 
Let $\map \CC I$ be the set of continuous functions on $I$. 
Let $\map \DD I$ be the set of continuous functions on $I$ that are differentiable at a point.
Let $d$ be the metric induced by the supremum norm.
Then $\map \DD I$ is meager in $\struct {\map \CC I, d}$.

Proof:
Let: 
:$\ds A_{n, m} = \set {f \in \map \CC I: \exists x \in I: \forall t \in I: 0 < \size {t - x} < \frac 1 m \implies \size {\frac {\map f t - \map f x} {t - x} } \le n}$
and:
:$\ds A = \bigcup_{\tuple {n, m} \mathop \in \N^2} A_{n, m}$
Theorem: Space of Somewhere Differentiable Continuous Functions on Closed Interval is Meager in Space of Continuous Functions on Closed Interval/Lemma 1

:$\map \DD I \subseteq A$

Proof:
Let $f \in \map \DD I$. 
Then, $f$ is differentiable at some $x \in I$.
Let: 
:$n = \floor {\size {\map {f'} x} } + 1$
where $\floor \cdot$ is the floor function.
Then:
:$\size {\map {f'} x} < n$
From the definition of the derivative, there exists $\delta > 0$ such that for all $t$ with $0 < \size {t - x} < \delta$, we have: 
:$\ds \size {\frac {\map f t - \map f x} {t - x} - \map {f'} x} < 1 - \fractpart {\size {\map {f'} x} }$
From the Reverse Triangle Inequality, we then have: 
:$\ds \size {\size {\frac {\map f t - \map f x} {t - x} } - \size {\map {f'} x} } < 1 - \fractpart {\size {\map {f'} x} }$
and so:
{{begin-eqn}}
{{eqn | l = \size {\frac {\map f t - \map f x} {t - x} }
      | o = <
      | r = \size {\map {f'} x} - \fractpart {\size {\map {f'} x} } + 1
}}
{{eqn | r = \floor {\size {\map {f'} x} } + 1
      | c = {{Defof|Fractional Part}}
}}
{{eqn | r = n
}}
{{end-eqn}}
for all $t$ with $0 < \size {t - x} < \delta$.
Pick $m \in \N$ such that $\frac 1 m < \delta$.
We then have:
:$\ds \size {\frac {\map f t - \map f x} {t - x} } \le n$
for $t$ with $0 < \size {t - x} < \frac 1 m$.
That is:
:$f \in A_{n, \, m} \subseteq A$
so:
:$\map \DD I \subseteq A$
as required.
{{qed}}
Category:Space of Somewhere Differentiable Continuous Functions on Closed Interval is Meager in Space of Continuous Functions on Closed Interval
rabkg7sn6fg0hyougsjguhe00dhh5ap
Theorem: Space of Somewhere Differentiable Continuous Functions on Closed Interval is Meager in Space of Continuous Functions on Closed Interval/Corollary

:there exists a function $f \in \map \CC I$ that is not differentiable anywhere.

Proof:
Let $\map \DD I$ be the set of continuous functions on $I$ that are differentiable at a point.
Let $d$ be the metric induced by the supremum norm.
By Space of Continuous on Closed Interval Real-Valued Functions with Supremum Norm forms Banach Space:
:$\struct {\map \CC I, d}$ is a complete metric space.
By Baire Space is Non-Meager:
:$\map \CC I$ is non-meager in $\struct {\map \CC I, d}$.
By Space of Somewhere Differentiable Continuous Functions on Closed Interval is Meager in Space of Continuous Functions on Closed Interval:
:$\map \DD I$ is meager in $\struct {\map \CC I, d}$.
So:
:$\map \DD I \ne \map \CC I$.
That is, there exists a continuous function that is not differentiable anywhere.
{{qed}}
Theorem: Max Operation is Commutative

The Max operation is commutative:
:$\map \max {x, y} = \map \max {y, x}$

Proof:
To simplify our notation:
:Let $\map \max {x, y}$ be (temporarily) denoted $x \overline \wedge y$
There are three cases to consider:
:$(1): \quad x \le y$
:$(2): \quad y \le x$
:$(3): \quad x = y$
$(1): \quad$ Let $x \le y$.
Then:
{{begin-eqn}}
{{eqn | l = x \overline \wedge y
      | r = y
      | rr= = y \overline \wedge x
}}
{{end-eqn}}
$(2): \quad$ Let $y \le x$.
Then:
{{begin-eqn}}
{{eqn | l = x \overline \wedge y
      | r = x
      | rr= = y \overline \wedge x
}}
{{end-eqn}}
$(3): \quad$ Let $x = y$.
Then:
{{begin-eqn}}
{{eqn | l = x \overline \wedge y
      | r = x = y
      | rr= = y \overline \wedge x
}}
{{end-eqn}}
Thus $\overline \wedge$, that is $\max$, has been shown to be commutative in all cases.
{{qed}}
Theorem: Min Operation is Commutative

The Min operation is commutative:
:$\map \min {x, y} = \map \min {y, x}$

Proof:
To simplify our notation:
:Let $\map \min {x, y}$ be (temporarily) denoted $x \underline \vee y$.
There are three cases to consider:
:$(1): \quad x \le y$
:$(2): \quad y \le x$
:$(3): \quad x = y$
$(1): \quad$ Let $x \le y$.
Then:
{{begin-eqn}}
{{eqn | l = x \underline \vee y
      | r = x
      | rr= =y \underline \vee x
}}
{{end-eqn}}
$(2): \quad$ Let $y \le x$.
Then:
{{begin-eqn}}
{{eqn | l = x \underline \vee y
      | r = y
      | rr= =y \underline \vee x
}}
{{end-eqn}}
$(3): \quad$ Let $x = y$.
Then:
{{begin-eqn}}
{{eqn | l = x \underline \vee y
      | r = x = y
      | rr= =y \underline \vee x
}}
{{end-eqn}}
Thus $\underline \vee$, i.e. $\min$, has been shown to be commutative in all cases.
{{qed}}