Proof Machine
Arun Ram
Department of Mathematics and Statistics
University of Melbourne
Parkville, VIC 3010 Australia
aram@unimelb.edu.au
A talk at University of Melbourne
7 March 2014
toggle mathjax on/off
medic
|
Assume the ifs |
To show: the thens |
|
Proof type II:
To show: If A then B .
The next lines are
Let
be a function. Show that is invertible
is a bijection.
|
|
Proof. |
|
- To show: (a) If is invertible then is a bijection.
-
(b) If is a bijection then is invertible.
- (a) Assume is invertible.
-
To show: is a bijection.
-
We know: There exists such that
-
To show: (aa) is injective.
-
(ab) is surjective.
-
(aa) To show: If and
then
.
-
Assume and
.
-
To show: .
(proof type I)
-
So is injective.
-
(ab) To show: is surjective.
-
To show:
If then there exists
such that
.
-
Assume .
-
To show: There exists
such that
.
(proof type III)
-
Define .
-
To show: .
-
So is surjective.
- So is bijective.
- (b) To sh....
- .
- .
- .
- .
|
Proof type I: LHS = RHS.
The next lines are
- LHS
= ⋯
= ⋯
= ⋯
= ⋯
=
.
- RHS
= ⋯
= ⋯
= ⋯
= ⋯
=
.
Prove that .
|
|
Proof. |
|
|
Proof type III:
There exists C such that D .
The next lines are
- Define C = xxx .
- To show:
D .
Prove that is continuous at 0.
|
|
Proof. |
|
- To show: .
-
- To show: .
- To show: If
then there exists
such that if
then
.
- Assume
.
- To show:
There exists
such that if
then
.
- Define .
- To show:
If
then
.
- Assume
.
- To show:
.
|
|
Special kinds of proofs
- Proofs of uniqueness ()
- Contradiction or contrapositive
- Proofs of presentations (generators and relations)
- Proofs by induction (the definition of !!!)
- Proof by intimidation (the most common and least rigourous)
|
Definitions
- Format:
- A noun is an object such that condition.
- An adjective noun is a such that condition.
- A condition or statement can only be in the form
-
- If A then
B
- or
- There exists C such that
condition .
-
- Definitions can change!
- "What's the definition of a Schur function?!?!!"
- The challenge of taking on a definition.
- "They're made out of meat"
|
Extra stuff
- How did you come to formalise Proof Machine?
- My notes page: Google "Arun Ram Notes"
|
top
The medical doctor
Before you try Lindelöf we need to an
assessment on your
results to check that there is no underlying
in the
.
Believe me, ending up Lipschitz is no fun for anyone.