Sets and Logic
1.3 Relations
1.3.1 The Law of the Excluded Middle
The Law of the Excluded Middle states that for any proposition $P$, either $P$, or its negation $¬ P$ is true.
Theorem
If $P$ is a proposition, then $ ¬ (¬ P) ⇔ P$.
theorem not_not_P_is_P
(P : Prop) : ¬ (¬ P) ↔ P :=
Proof
QED.
We need to show that $¬ (¬ P)$ is true 'if and only if' $P$ is true. So we consider both directions of the implication.
split,
P : Prop
⊢ ¬¬P ↔ P
2 goals
P : Prop
⊢ ¬¬P → P
P : Prop
⊢ P → ¬¬P
Let's first consider the forward implication, i.e. $¬ (¬ P)$ is true implies that $P$ is also true.
intro hp,
2 goals
P : Prop
⊢ ¬¬P → P
P : Prop
⊢ P → ¬¬P
2 goals
P : Prop,
hp : ¬¬P
⊢ P
P : Prop
⊢ P → ¬¬P
We will prove this by contradiction so given $¬ (¬ P)$ is true let's make a dubious assumption that $¬ P$ is true.
apply classical.by_contradiction,
2 goals
P : Prop,
hp : ¬¬P
⊢ P
P : Prop
⊢ P → ¬¬P
2 goals
P : Prop,
hp : ¬¬P
⊢ ¬P → false
P : Prop
⊢ P → ¬¬P
intro hnp,
2 goals
P : Prop,
hp : ¬¬P
⊢ ¬P → false
P : Prop
⊢ P → ¬¬P
2 goals
P : Prop,
hp : ¬¬P,
hnp : ¬P
⊢ false
P : Prop
⊢ P → ¬¬P
But $¬ P$ is true implies that $¬ (¬ P)$ is false which is a contradiction to our premis that $¬ (¬ P)$ is true. Thus, $¬ P$ must be false which by the Law of the excluded middle implies $P$ is true, resulting in the first part of the proof!
contradiction,
2 goals
P : Prop,
hp : ¬¬P,
hnp : ¬P
⊢ false
P : Prop
⊢ P → ¬¬P
P : Prop
⊢ P → ¬¬P
Now we need to proof that the backwards implication is also correct, i.e. $P$ is true implies $¬ (¬ P)$ is also true. To show that $¬ (¬ P)$ is true when $P$ is true, we can simply show that $P$ is true implies $¬ P$ is false.
intros hp hnp,
P : Prop
⊢ P → ¬¬P
P : Prop,
hp : P,
hnp : ¬P
⊢ false
But this is true by definition, so we have nothing left to prove!
contradiction,
P : Prop,
hp : P,
hnp : ¬P
⊢ false
no goals
Remark. Note that for many simple propositions alike the one above, LEAN is able to use automation to complete our proof. Indeed, by using the tactic $\tt{finish}$, the above proof becomes a one-liner!
Theorem
If $P$ is a proposition, then $ ¬ (¬ P) ⇔ P$. (This time proven using $\tt{finish}$)
theorem not_not_P_is_P_tauto
(P : Prop) : ¬ (¬ P) ↔ P :=
Proof
QED.
As we can see, $\tt{finish}$ finished the proof!
finish
P : Prop
⊢ ¬¬P ↔ P
P : Prop
⊢ ¬¬P ↔ P
1.3.2 De Morgan's Laws
Theorem
(1) Let $P$ and $Q$ be propositions, then $¬ (P ∨ Q) ⇔ (¬ P) ∧ (¬ Q)$
theorem demorgan_a
(P Q : Prop) : ¬ (P ∨ Q) ↔ (¬ P) ∧ (¬ Q) :=
Proof
QED.
Again we have an 'if and only if' statement so we need to consider both directions of the argument.
split,
P Q : Prop
⊢ ¬(P ∨ Q) ↔ ¬P ∧ ¬Q
2 goals
P Q : Prop
⊢ ¬(P ∨ Q) → ¬P ∧ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
We first show that $¬ (P ∨ Q) ⇒ ¬ P ∧ ¬ Q$ through contradiction. Suppose $¬ (P ∨ Q)$ is true, and we make a dubious assumption that $P$ is true.
intro h,
2 goals
P Q : Prop
⊢ ¬(P ∨ Q) → ¬P ∧ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
2 goals
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬P ∧ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
split,
2 goals
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬P ∧ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
3 goals
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬P
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
intro hp,
3 goals
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬P
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
3 goals
P Q : Prop,
h : ¬(P ∨ Q),
hp : P
⊢ false
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
But then $¬ (P ∨ Q)$ is false! A contradiction! Therefore $P$ must be false.
apply h,
3 goals
P Q : Prop,
h : ¬(P ∨ Q),
hp : P
⊢ false
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
3 goals
P Q : Prop,
h : ¬(P ∨ Q),
hp : P
⊢ P ∨ Q
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
left, exact hp,
3 goals
P Q : Prop,
h : ¬(P ∨ Q),
hp : P
⊢ P ∨ Q
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
2 goals
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
Similarly, supposing $Q$ is true also results in a contradiction! Therefore $Q$ is also false.
intro hq,
2 goals
P Q : Prop,
h : ¬(P ∨ Q)
⊢ ¬Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
2 goals
P Q : Prop,
h : ¬(P ∨ Q),
hq : Q
⊢ false
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
apply h,
2 goals
P Q : Prop,
h : ¬(P ∨ Q),
hq : Q
⊢ false
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
2 goals
P Q : Prop,
h : ¬(P ∨ Q),
hq : Q
⊢ P ∨ Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
right, exact hq,
2 goals
P Q : Prop,
h : ¬(P ∨ Q),
hq : Q
⊢ P ∨ Q
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
With that, we now focus our attention on the backwards implication, i.e. $(¬ P) ∧ (¬ Q) ⇒ ¬ (P ∨ Q)$. Again, let's approach this by contradiction. Given $¬ P ∧ ¬ Q$ suppose we have $P$ or $Q$.
intros h hpq,
P Q : Prop
⊢ ¬P ∧ ¬Q → ¬(P ∨ Q)
P Q : Prop,
h : ¬P ∧ ¬Q,
hpq : P ∨ Q
⊢ false
But $P$ can't be true, as we have $¬ P$,
cases h with hnp hnq,
P Q : Prop,
h : ¬P ∧ ¬Q,
hpq : P ∨ Q
⊢ false
P Q : Prop,
hpq : P ∨ Q,
hnp : ¬P,
hnq : ¬Q
⊢ false
cases hpq with hp hq,
P Q : Prop,
hpq : P ∨ Q,
hnp : ¬P,
hnq : ¬Q
⊢ false
2 goals
case or.inl
P Q : Prop,
hnp : ¬P,
hnq : ¬Q,
hp : P
⊢ false
case or.inr
P Q : Prop,
hnp : ¬P,
hnq : ¬Q,
hq : Q
⊢ false
contradiction,
2 goals
case or.inl
P Q : Prop,
hnp : ¬P,
hnq : ¬Q,
hp : P
⊢ false
case or.inr
P Q : Prop,
hnp : ¬P,
hnq : ¬Q,
hq : Q
⊢ false
case or.inr
P Q : Prop,
hnp : ¬P,
hnq : ¬Q,
hq : Q
⊢ false
Therefore, $Q$ must be true. But $Q$ also can't be true as we have $¬ Q$! Contradiction! Therefore, given $(¬ P) ∧ (¬ Q)$, $(P ∨ Q)$ must not be true, i.e. $¬ (P ∨ Q)$ is true, which is exactly what we need!
contradiction,
case or.inr
P Q : Prop,
hnp : ¬P,
hnq : ¬Q,
hq : Q
⊢ false
no goals
Theorem
(2) Let $P$ and $Q$ be propositions, then $¬ (P ∧ Q) ⇔ (¬ P) ∨ (¬ Q)$
theorem demorgan_b
(P Q : Prop) : ¬ (P ∧ Q) ↔ (¬ P) ∨ (¬ Q) :=
Proof
QED.
Once again, we have an 'if and only' if statement, therefore, we need to consider both directions.
split,
P Q : Prop
⊢ ¬(P ∧ Q) ↔ ¬P ∨ ¬Q
2 goals
P Q : Prop
⊢ ¬(P ∧ Q) → ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
We first show that $¬ (P ∧ Q) ⇒ ¬ P ∨ ¬ Q$. Suppose $¬ (P ∧ Q)$.
intro h,
2 goals
P Q : Prop
⊢ ¬(P ∧ Q) → ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
2 goals
P Q : Prop,
h : ¬(P ∧ Q)
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
By the law of the excluded middle, we have either $P$ or $¬ P$.
cases (classical.em P) with hp hnp,
2 goals
P Q : Prop,
h : ¬(P ∧ Q)
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
3 goals
case or.inl
P Q : Prop,
h : ¬(P ∧ Q),
hp : P
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
Suppose first that we have $P$. Then, we must have $¬ Q$ as having $Q$ implies $P ∧ Q$ which contradicts with $¬ (P ∧ Q)$,
have hnq : ¬ Q,
3 goals
case or.inl
P Q : Prop,
h : ¬(P ∧ Q),
hp : P
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
4 goals
P Q : Prop,
h : ¬(P ∧ Q),
hp : P
⊢ ¬Q
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hnq : ¬Q
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
intro hq,
4 goals
P Q : Prop,
h : ¬(P ∧ Q),
hp : P
⊢ ¬Q
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hnq : ¬Q
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
4 goals
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hq : Q
⊢ false
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hnq : ¬Q
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
have hpq : P ∧ Q,
4 goals
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hq : Q
⊢ false
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hnq : ¬Q
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
5 goals
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hq : Q
⊢ P ∧ Q
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hq : Q,
hpq : P ∧ Q
⊢ false
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hnq : ¬Q
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
split, exact hp, exact hq,
5 goals
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hq : Q
⊢ P ∧ Q
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hq : Q,
hpq : P ∧ Q
⊢ false
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hnq : ¬Q
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
4 goals
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hq : Q,
hpq : P ∧ Q
⊢ false
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hnq : ¬Q
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
contradiction,
4 goals
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hq : Q,
hpq : P ∧ Q
⊢ false
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hnq : ¬Q
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
3 goals
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hnq : ¬Q
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
hence, we have $¬ P ∨ ¬ Q$.
right, exact hnq,
3 goals
P Q : Prop,
h : ¬(P ∧ Q),
hp : P,
hnq : ¬Q
⊢ ¬P ∨ ¬Q
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
2 goals
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
Now let's suppose $¬ P$. But as $¬ P$ implies $¬ P ∨ ¬ Q$, we have nothing left to prove.
left, exact hnp,
2 goals
case or.inr
P Q : Prop,
h : ¬(P ∧ Q),
hnp : ¬P
⊢ ¬P ∨ ¬Q
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
With the forward implication dealt with, let's consider the reverse, i.e. $¬ P ∨ ¬ Q ⇒ ¬ (P ∧ Q)$. Given $¬ P ∨ ¬ Q$ let's suppose that $P ∧ Q$.
intros h hpq,
P Q : Prop
⊢ ¬P ∨ ¬Q → ¬(P ∧ Q)
P Q : Prop,
h : ¬P ∨ ¬Q,
hpq : P ∧ Q
⊢ false
But this is a contradiction as $P ∧ Q$ implies that neither $P$ nor $Q$ is false!
cases h with hnp hnq,
P Q : Prop,
h : ¬P ∨ ¬Q,
hpq : P ∧ Q
⊢ false
2 goals
case or.inl
P Q : Prop,
hpq : P ∧ Q,
hnp : ¬P
⊢ false
case or.inr
P Q : Prop,
hpq : P ∧ Q,
hnq : ¬Q
⊢ false
cases hpq with hp hq,
2 goals
case or.inl
P Q : Prop,
hpq : P ∧ Q,
hnp : ¬P
⊢ false
case or.inr
P Q : Prop,
hpq : P ∧ Q,
hnq : ¬Q
⊢ false
2 goals
P Q : Prop,
hnp : ¬P,
hp : P,
hq : Q
⊢ false
case or.inr
P Q : Prop,
hpq : P ∧ Q,
hnq : ¬Q
⊢ false
contradiction,
2 goals
P Q : Prop,
hnp : ¬P,
hp : P,
hq : Q
⊢ false
case or.inr
P Q : Prop,
hpq : P ∧ Q,
hnq : ¬Q
⊢ false
case or.inr
P Q : Prop,
hpq : P ∧ Q,
hnq : ¬Q
⊢ false
cases hpq with hp hq,
case or.inr
P Q : Prop,
hpq : P ∧ Q,
hnq : ¬Q
⊢ false
P Q : Prop,
hnq : ¬Q,
hp : P,
hq : Q
⊢ false
Therefore, $P ∧ Q$ must be false by contradiction which results in the second part of our proof!
contradiction,
P Q : Prop,
hnq : ¬Q,
hp : P,
hq : Q
⊢ false
no goals
Excercise. As you can see, writing LEAN proofs is so much more fun than drawing truth tables! Why don't you try it out by proving $\lnot P \iff (P \implies \tt{false})$ here?
1.3.3 Transitivity of Implications, and the Contrapositive
Theorem
$⇒$ is transitive, i.e. if $P$, $Q$, and $R$ are propositions, then $P ⇒ Q$ and $Q ⇒ R$ means $P ⇒ R$.
theorem imp_trans
(P Q R : Prop) : (P → Q) ∧ (Q → R) → (P → R) :=
Proof
QED.
Suppose $P ⇒ Q$ and $Q ⇒ R$ are both true, we then would like to prove that $P ⇒ R$ is true.
intro h,
P Q R : Prop
⊢ (P → Q) ∧ (Q → R) → P → R
P Q R : Prop,
h : (P → Q) ∧ (Q → R)
⊢ P → R
cases h with hpq hqr,
P Q R : Prop,
h : (P → Q) ∧ (Q → R)
⊢ P → R
P Q R : Prop,
hpq : P → Q,
hqr : Q → R
⊢ P → R
Say that $P$ is true,
intro hp,
P Q R : Prop,
hpq : P → Q,
hqr : Q → R
⊢ P → R
P Q R : Prop,
hpq : P → Q,
hqr : Q → R,
hp : P
⊢ R
then by $P ⇒ Q$, $Q$ must be true. But we also have $Q ⇒ R$, therefore $R$ is also true, which is exactly what we wish to prove!
exact hqr (hpq hp),
P Q R : Prop,
hpq : P → Q,
hqr : Q → R,
hp : P
⊢ R
no goals
Theorem
If $P$ and $Q$ are propositions, then $(P ⇒ Q) ⇔ (¬ Q ⇒ ¬ P)$.
theorem contra
(P Q : Prop) : (P → Q) ↔ (¬ Q → ¬ P) :=
Proof
QED.
Let's first consider the implication from left to right, i.e. $(P ⇒ Q) ⇒ (¬ Q ⇒ ¬ P)$.
split,
P Q : Prop
⊢ P → Q ↔ ¬Q → ¬P
2 goals
P Q : Prop
⊢ (P → Q) → ¬Q → ¬P
P Q : Prop
⊢ (¬Q → ¬P) → P → Q
We will prove this by contradiction, so suppose we have $P ⇒ Q$, $¬ Q$ and not $¬ P$.
intros h hnq hp,
2 goals
P Q : Prop
⊢ (P → Q) → ¬Q → ¬P
P Q : Prop
⊢ (¬Q → ¬P) → P → Q
2 goals
P Q : Prop,
h : P → Q,
hnq : ¬Q,
hp : P
⊢ false
P Q : Prop
⊢ (¬Q → ¬P) → P → Q
But not $¬ P$ is simply $P$, and $P$ implies $Q$, a contradiction to $¬ Q$! Therefore, $P ⇒ Q$ must imply $¬ Q ⇒ ¬ P$ as required.
exact hnq (h hp),
2 goals
P Q : Prop,
h : P → Q,
hnq : ¬Q,
hp : P
⊢ false
P Q : Prop
⊢ (¬Q → ¬P) → P → Q
P Q : Prop
⊢ (¬Q → ¬P) → P → Q
Now lets consider reverse, $(¬ Q ⇒ ¬ P) ⇒ (P ⇒ Q)$. Suppose we have $¬ Q ⇒ ¬ P$ and $P$.
intros h hp,
P Q : Prop
⊢ (¬Q → ¬P) → P → Q
P Q : Prop,
h : ¬Q → ¬P,
hp : P
⊢ Q
If $Q$ is true then we have nothing left to prove, so suppose $¬ Q$ is true.
cases (classical.em Q) with hq hnq,
P Q : Prop,
h : ¬Q → ¬P,
hp : P
⊢ Q
2 goals
case or.inl
P Q : Prop,
h : ¬Q → ¬P,
hp : P,
hq : Q
⊢ Q
case or.inr
P Q : Prop,
h : ¬Q → ¬P,
hp : P,
hnq : ¬Q
⊢ Q
exact hq,
2 goals
case or.inl
P Q : Prop,
h : ¬Q → ¬P,
hp : P,
hq : Q
⊢ Q
case or.inr
P Q : Prop,
h : ¬Q → ¬P,
hp : P,
hnq : ¬Q
⊢ Q
case or.inr
P Q : Prop,
h : ¬Q → ¬P,
hp : P,
hnq : ¬Q
⊢ Q
exfalso,
case or.inr
P Q : Prop,
h : ¬Q → ¬P,
hp : P,
hnq : ¬Q
⊢ Q
P Q : Prop,
h : ¬Q → ¬P,
hp : P,
hnq : ¬Q
⊢ false
But $¬ Q$ implies $¬ P$ which contradicts with $P$, therefore, $¬ Q$ must be false as requied.
exact h hnq hp,
P Q : Prop,
h : ¬Q → ¬P,
hp : P,
hnq : ¬Q
⊢ false
no goals
Excercise. What can we deduce if we apply the contrapositive to $\lnot Q \implies \lnot P$? Try it out here?
1.3.4 Distributivity
Theorem
(1) If $P$, $Q$, and $R$ are propositions. Then, $P ∧ (Q ∨ R) ⇔ (P ∧ Q) ∨ (P ∧ R)$;
theorem dis_and_or
(P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) :=
Proof
QED.
Let's first consider the foward implication, $P ∧ (Q ∨ R) ⇒ (P ∧ Q) ∨ (P ∧ R)$
split,
P Q R : Prop
⊢ P ∧ (Q ∨ R) ↔ P ∧ Q ∨ P ∧ R
2 goals
P Q R : Prop
⊢ P ∧ (Q ∨ R) → P ∧ Q ∨ P ∧ R
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
Suppose $P$ is true and either $Q$ or $R$ is true.
rintro ⟨hp, hqr⟩,
2 goals
P Q R : Prop
⊢ P ∧ (Q ∨ R) → P ∧ Q ∨ P ∧ R
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
2 goals
P Q R : Prop,
hp : P,
hqr : Q ∨ R
⊢ P ∧ Q ∨ P ∧ R
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
But this means either $P$ and $Q$ is true or $P$ and $R$ is true which is exactly what we need.
cases hqr with hq hr,
2 goals
P Q R : Prop,
hp : P,
hqr : Q ∨ R
⊢ P ∧ Q ∨ P ∧ R
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
3 goals
case or.inl
P Q R : Prop,
hp : P,
hq : Q
⊢ P ∧ Q ∨ P ∧ R
case or.inr
P Q R : Prop,
hp : P,
hr : R
⊢ P ∧ Q ∨ P ∧ R
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
left, split, repeat {assumption},
3 goals
case or.inl
P Q R : Prop,
hp : P,
hq : Q
⊢ P ∧ Q ∨ P ∧ R
case or.inr
P Q R : Prop,
hp : P,
hr : R
⊢ P ∧ Q ∨ P ∧ R
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
2 goals
case or.inr
P Q R : Prop,
hp : P,
hr : R
⊢ P ∧ Q ∨ P ∧ R
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
right, split, repeat {assumption},
2 goals
case or.inr
P Q R : Prop,
hp : P,
hr : R
⊢ P ∧ Q ∨ P ∧ R
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
With that, we now need to prove the backwards implication. Suppose $(P ∧ Q) ∨ (P ∧ R)$.
intro h,
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
P Q R : Prop,
h : P ∧ Q ∨ P ∧ R
⊢ P ∧ (Q ∨ R)
Let's consider both cases.
cases h with hpq hpr,
P Q R : Prop,
h : P ∧ Q ∨ P ∧ R
⊢ P ∧ (Q ∨ R)
2 goals
case or.inl
P Q R : Prop,
hpq : P ∧ Q
⊢ P ∧ (Q ∨ R)
case or.inr
P Q R : Prop,
hpr : P ∧ R
⊢ P ∧ (Q ∨ R)
If $P ∧ Q$ is true, then $P$ is true and $Q ∨ R$ is also true.
cases hpq with hp hq,
2 goals
case or.inl
P Q R : Prop,
hpq : P ∧ Q
⊢ P ∧ (Q ∨ R)
case or.inr
P Q R : Prop,
hpr : P ∧ R
⊢ P ∧ (Q ∨ R)
2 goals
P Q R : Prop,
hp : P,
hq : Q
⊢ P ∧ (Q ∨ R)
case or.inr
P Q R : Prop,
hpr : P ∧ R
⊢ P ∧ (Q ∨ R)
split, assumption, left, assumption,
2 goals
P Q R : Prop,
hp : P,
hq : Q
⊢ P ∧ (Q ∨ R)
case or.inr
P Q R : Prop,
hpr : P ∧ R
⊢ P ∧ (Q ∨ R)
case or.inr
P Q R : Prop,
hpr : P ∧ R
⊢ P ∧ (Q ∨ R)
Similarly, is $P ∧ R$ is true, then $P$ is true and $Q ∨ R$ is also true.
cases hpr with hp hr,
case or.inr
P Q R : Prop,
hpr : P ∧ R
⊢ P ∧ (Q ∨ R)
P Q R : Prop,
hp : P,
hr : R
⊢ P ∧ (Q ∨ R)
Therefore, by considering bothe cases, we see that either $P ∧ Q$ or $P ∧ R$ implies $P ∧ (Q ∨ R)$.
split, assumption, right, assumption,
P Q R : Prop,
hp : P,
hr : R
⊢ P ∧ (Q ∨ R)
no goals
Theorem
(2) $P ∨ (Q ∧ R) ⇔ (P ∨ Q) ∧ (P ∨ R)$.
theorem dis_or_and
(P Q R : Prop) : P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R) :=
Proof
QED.
We first consider the forward implication $P ∨ (Q ∧ R) ⇒ (P ∨ Q) ∧ (P ∨ R)$.
split,
P Q R : Prop
⊢ P ∨ Q ∧ R ↔ (P ∨ Q) ∧ (P ∨ R)
2 goals
P Q R : Prop
⊢ P ∨ Q ∧ R → (P ∨ Q) ∧ (P ∨ R)
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
Suppose we have $P ∨ (Q ∧ R)$, then either $P$ is true or $Q$ and $R$ is true$.
intro h,
2 goals
P Q R : Prop
⊢ P ∨ Q ∧ R → (P ∨ Q) ∧ (P ∨ R)
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
2 goals
P Q R : Prop,
h : P ∨ Q ∧ R
⊢ (P ∨ Q) ∧ (P ∨ R)
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
Let's consider both cases. If $P$ is true, then both $P ∨ Q$ and $P ∨ R$ are true.
cases h with hp hqr,
2 goals
P Q R : Prop,
h : P ∨ Q ∧ R
⊢ (P ∨ Q) ∧ (P ∨ R)
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
3 goals
case or.inl
P Q R : Prop,
hp : P
⊢ (P ∨ Q) ∧ (P ∨ R)
case or.inr
P Q R : Prop,
hqr : Q ∧ R
⊢ (P ∨ Q) ∧ (P ∨ R)
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
split, repeat {left, assumption},
3 goals
case or.inl
P Q R : Prop,
hp : P
⊢ (P ∨ Q) ∧ (P ∨ R)
case or.inr
P Q R : Prop,
hqr : Q ∧ R
⊢ (P ∨ Q) ∧ (P ∨ R)
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
2 goals
case or.inr
P Q R : Prop,
hqr : Q ∧ R
⊢ (P ∨ Q) ∧ (P ∨ R)
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
Similarly, if $P$ and $Q$ are true, then both $P ∨ Q$ and $P ∨ R$ are true.
cases hqr with hq hr,
2 goals
case or.inr
P Q R : Prop,
hqr : Q ∧ R
⊢ (P ∨ Q) ∧ (P ∨ R)
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
2 goals
P Q R : Prop,
hq : Q,
hr : R
⊢ (P ∨ Q) ∧ (P ∨ R)
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
split, repeat {right, assumption},
2 goals
P Q R : Prop,
hq : Q,
hr : R
⊢ (P ∨ Q) ∧ (P ∨ R)
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
Now let's consider the backwards implication. Suppose that $(P ∨ Q)$ and $(P ∨ R)$ is true and lets consider all the cases.
intro h,
P Q R : Prop
⊢ (P ∨ Q) ∧ (P ∨ R) → P ∨ Q ∧ R
P Q R : Prop,
h : (P ∨ Q) ∧ (P ∨ R)
⊢ P ∨ Q ∧ R
cases h with hpq hpr,
P Q R : Prop,
h : (P ∨ Q) ∧ (P ∨ R)
⊢ P ∨ Q ∧ R
P Q R : Prop,
hpq : P ∨ Q,
hpr : P ∨ R
⊢ P ∨ Q ∧ R
If $P$ is true the $P ∨ (Q ∧ R)$ is also true.
cases hpq with hp hq,
P Q R : Prop,
hpq : P ∨ Q,
hpr : P ∨ R
⊢ P ∨ Q ∧ R
2 goals
case or.inl
P Q R : Prop,
hpr : P ∨ R,
hp : P
⊢ P ∨ Q ∧ R
case or.inr
P Q R : Prop,
hpr : P ∨ R,
hq : Q
⊢ P ∨ Q ∧ R
cases hpr with hp hr,
2 goals
case or.inl
P Q R : Prop,
hpr : P ∨ R,
hp : P
⊢ P ∨ Q ∧ R
case or.inr
P Q R : Prop,
hpr : P ∨ R,
hq : Q
⊢ P ∨ Q ∧ R
3 goals
case or.inl
P Q R : Prop,
hp hp : P
⊢ P ∨ Q ∧ R
case or.inr
P Q R : Prop,
hp : P,
hr : R
⊢ P ∨ Q ∧ R
case or.inr
P Q R : Prop,
hpr : P ∨ R,
hq : Q
⊢ P ∨ Q ∧ R
repeat {left, assumption},
3 goals
case or.inl
P Q R : Prop,
hp hp : P
⊢ P ∨ Q ∧ R
case or.inr
P Q R : Prop,
hp : P,
hr : R
⊢ P ∨ Q ∧ R
case or.inr
P Q R : Prop,
hpr : P ∨ R,
hq : Q
⊢ P ∨ Q ∧ R
case or.inr
P Q R : Prop,
hpr : P ∨ R,
hq : Q
⊢ P ∨ Q ∧ R
If $¬ P$ is true then from $(P ∨ Q)$ and $(P ∨ R)$, $Q$ and $R$ must be true, and therefore, $P ∨ (Q ∧ R)$ is also true.
cases hpr with hp hr,
case or.inr
P Q R : Prop,
hpr : P ∨ R,
hq : Q
⊢ P ∨ Q ∧ R
2 goals
case or.inl
P Q R : Prop,
hq : Q,
hp : P
⊢ P ∨ Q ∧ R
case or.inr
P Q R : Prop,
hq : Q,
hr : R
⊢ P ∨ Q ∧ R
left, assumption,
2 goals
case or.inl
P Q R : Prop,
hq : Q,
hp : P
⊢ P ∨ Q ∧ R
case or.inr
P Q R : Prop,
hq : Q,
hr : R
⊢ P ∨ Q ∧ R
case or.inr
P Q R : Prop,
hq : Q,
hr : R
⊢ P ∨ Q ∧ R
right, split, repeat {assumption},
case or.inr
P Q R : Prop,
hq : Q,
hr : R
⊢ P ∨ Q ∧ R
no goals
1.7 Sets and Propositions
Theorem
(1) $\bar{X ∪ Y} = \bar{X} ∩ \bar{Y}$.
theorem de_morg_set_a (X Y : set Ω) : - (X ∪ Y) = - X ∩ - Y :=
Proof
QED.
What exactly does $\bar{(X ∪ Y)}$ and $\bar{X} ∩ \bar{Y}$ mean? Well, lets find out!
ext,
Ω : Type u_1,
X Y : set Ω
⊢ -(X ∪ Y) = -X ∩ -Y
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -(X ∪ Y) ↔ x ∈ -X ∩ -Y
As we can see, to show that $\bar{X ∪ Y} = \bar{X} ∩ \bar{Y}$, we in fact need to prove $x ∈ \bar{(X ∪ Y)} ↔ x ∈ \bar{X} ∩ \bar{Y}$.
split,
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -(X ∪ Y) ↔ x ∈ -X ∩ -Y
2 goals
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -(X ∪ Y) → x ∈ -X ∩ -Y
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -X ∩ -Y → x ∈ -(X ∪ Y)
So let's first prove that $x ∈ \bar{X ∪ Y} → x ∈ \bar{X} ∩ \bar{Y}$. Suppose $x ∈ \bar{X ∪ Y}$, then $x$ is not in $X$ and $x$ is not in $Y$.
dsimp, intro h,
2 goals
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -(X ∪ Y) → x ∈ -X ∩ -Y
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -X ∩ -Y → x ∈ -(X ∪ Y)
2 goals
Ω : Type u_1,
X Y : set Ω,
x : Ω,
h : ¬(x ∈ X ∨ x ∈ Y)
⊢ x ∉ X ∧ x ∉ Y
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -X ∩ -Y → x ∈ -(X ∪ Y)
push_neg at h,
2 goals
Ω : Type u_1,
X Y : set Ω,
x : Ω,
h : ¬(x ∈ X ∨ x ∈ Y)
⊢ x ∉ X ∧ x ∉ Y
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -X ∩ -Y → x ∈ -(X ∪ Y)
2 goals
Ω : Type u_1,
X Y : set Ω,
x : Ω,
h : x ∉ X ∧ x ∉ Y
⊢ x ∉ X ∧ x ∉ Y
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -X ∩ -Y → x ∈ -(X ∪ Y)
But this is exactly what we need!
assumption,
2 goals
Ω : Type u_1,
X Y : set Ω,
x : Ω,
h : x ∉ X ∧ x ∉ Y
⊢ x ∉ X ∧ x ∉ Y
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -X ∩ -Y → x ∈ -(X ∪ Y)
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -X ∩ -Y → x ∈ -(X ∪ Y)
Now, let's consider the backwards implication. Similarly, $x ∈ \bar{X} ∩ \bar{Y}$ means $x$ is not in $X$ and $x$ is not in $Y$.
dsimp, intro h,
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -X ∩ -Y → x ∈ -(X ∪ Y)
Ω : Type u_1,
X Y : set Ω,
x : Ω,
h : x ∉ X ∧ x ∉ Y
⊢ ¬(x ∈ X ∨ x ∈ Y)
But this is what $x ∈ \bar{X ∪ Y}$ means, so we're done!
push_neg,
Ω : Type u_1,
X Y : set Ω,
x : Ω,
h : x ∉ X ∧ x ∉ Y
⊢ ¬(x ∈ X ∨ x ∈ Y)
Ω : Type u_1,
X Y : set Ω,
x : Ω,
h : x ∉ X ∧ x ∉ Y
⊢ x ∉ X ∧ x ∉ Y
assumption
Ω : Type u_1,
X Y : set Ω,
x : Ω,
h : x ∉ X ∧ x ∉ Y
⊢ x ∉ X ∧ x ∉ Y
Ω : Type u_1,
X Y : set Ω,
x : Ω,
h : x ∉ X ∧ x ∉ Y
⊢ x ∉ X ∧ x ∉ Y
Theorem
(2) $\bar{X ∩ Y} = \bar{X} ∪ \bar{Y}$.
theorem de_morg_set_b (X Y : set Ω) : - (X ∩ Y) = - X ∪ - Y :=
Proof
QED.
Rather than proving this manually, why not try some automation this time.
ext, finish
Ω : Type u_1,
X Y : set Ω
⊢ -(X ∩ Y) = -X ∪ -Y
Ω : Type u_1,
X Y : set Ω,
x : Ω
⊢ x ∈ -(X ∩ Y) ↔ x ∈ -X ∪ -Y
Remark. Would you look at that! Proving the de Morgan's law with one single line. Now thats a nice proof if I ever seen one!
1.7.1 "For All" and "There Exists"
Theorem
Given a propositon $P$ whose truth value is dependent on $x ∈ X$, then $∀ x ∈ X, ¬ P(x) ⇔ ¬ (∃ x ∈ X, P(x))$, and
theorem neg_exist_is_all (X : Type) (P : X → Prop) : (∀ x : X, ¬ P x) ↔ ¬ (∃ x : X, P x) :=
Proof
QED.
(⇒) Let's first prove the forward implication, i.e. suppose that $∀ x ∈ X, ¬ P(x)$, we need to show that $¬ ∃ x ∈ X, P(x)$.
split,
X : Type,
P : X → Prop
⊢ (∀ (x : X), ¬P x) ↔ ¬∃ (x : X), P x
2 goals
X : Type,
P : X → Prop
⊢ (∀ (x : X), ¬P x) → (¬∃ (x : X), P x)
X : Type,
P : X → Prop
⊢ (¬∃ (x : X), P x) → ∀ (x : X), ¬P x
Let's prove this by contradiction! Let's suppose that $¬ ∃ x ∈ X, P(x)$ is in fact $\tt{false}$ and there is actually a $x$ out there where $P(x)$ is true!
rintro h ⟨x, hx⟩,
2 goals
X : Type,
P : X → Prop
⊢ (∀ (x : X), ¬P x) → (¬∃ (x : X), P x)
X : Type,
P : X → Prop
⊢ (¬∃ (x : X), P x) → ∀ (x : X), ¬P x
2 goals
X : Type,
P : X → Prop,
h : ∀ (x : X), ¬P x,
x : X,
hx : P x
⊢ false
X : Type,
P : X → Prop
⊢ (¬∃ (x : X), P x) → ∀ (x : X), ¬P x
But, by our assumption $∀ x ∈ X$, $P(x)$ is false, thus a contradiction!
from (h x) hx,
2 goals
X : Type,
P : X → Prop,
h : ∀ (x : X), ¬P x,
x : X,
hx : P x
⊢ false
X : Type,
P : X → Prop
⊢ (¬∃ (x : X), P x) → ∀ (x : X), ¬P x
X : Type,
P : X → Prop
⊢ (¬∃ (x : X), P x) → ∀ (x : X), ¬P x
(⇐) Now let's consider the other direction. Suppose that there does not exist a $x$ such that $P(x)$ is true, i.e. $¬ ∃ x ∈ X, P(x)$.
intro ha,
X : Type,
P : X → Prop
⊢ (¬∃ (x : X), P x) → ∀ (x : X), ¬P x
X : Type,
P : X → Prop,
ha : ¬∃ (x : X), P x
⊢ ∀ (x : X), ¬P x
Similarly, let's suppose that $∀ x ∈ X, ¬P x$ is not true.
intros x hx,
X : Type,
P : X → Prop,
ha : ¬∃ (x : X), P x
⊢ ∀ (x : X), ¬P x
X : Type,
P : X → Prop,
ha : ¬∃ (x : X), P x,
x : X,
hx : P x
⊢ false
But then, there must be a $x$ such that $P(x)$ is true, again, a contradiction!
have : ∃ (x : X), P x,
X : Type,
P : X → Prop,
ha : ¬∃ (x : X), P x,
x : X,
hx : P x
⊢ false
2 goals
X : Type,
P : X → Prop,
ha : ¬∃ (x : X), P x,
x : X,
hx : P x
⊢ ∃ (x : X), P x
X : Type,
P : X → Prop,
ha : ¬∃ (x : X), P x,
x : X,
hx : P x,
this : ∃ (x : X), P x
⊢ false
existsi x, assumption,
2 goals
X : Type,
P : X → Prop,
ha : ¬∃ (x : X), P x,
x : X,
hx : P x
⊢ ∃ (x : X), P x
X : Type,
P : X → Prop,
ha : ¬∃ (x : X), P x,
x : X,
hx : P x,
this : ∃ (x : X), P x
⊢ false
X : Type,
P : X → Prop,
ha : ¬∃ (x : X), P x,
x : X,
hx : P x,
this : ∃ (x : X), P x
⊢ false
contradiction,
X : Type,
P : X → Prop,
ha : ¬∃ (x : X), P x,
x : X,
hx : P x,
this : ∃ (x : X), P x
⊢ false
no goals
Theorem
$¬ (∀ x ∈ X, ¬ P(x)) ⇔ ∃ x ∈ X, P(x)$.
theorem neg_all_is_exist (X : Type) (P : X → Prop) : ¬ (∀ x : X, ¬ P x) ↔ ∃ x : X, P x :=
Proof
QED.
Now that we have gone through quite a lot of LEAN proofs, try to understand this one yourself!
split,
X : Type,
P : X → Prop
⊢ (¬∀ (x : X), ¬P x) ↔ ∃ (x : X), P x
2 goals
X : Type,
P : X → Prop
⊢ (¬∀ (x : X), ¬P x) → (∃ (x : X), P x)
X : Type,
P : X → Prop
⊢ (∃ (x : X), P x) → (¬∀ (x : X), ¬P x)
{intro h,
2 goals
X : Type,
P : X → Prop
⊢ (¬∀ (x : X), ¬P x) → (∃ (x : X), P x)
X : Type,
P : X → Prop
⊢ (∃ (x : X), P x) → (¬∀ (x : X), ¬P x)
X : Type,
P : X → Prop,
h : ¬∀ (x : X), ¬P x
⊢ ∃ (x : X), P x
apply classical.by_contradiction,
X : Type,
P : X → Prop,
h : ¬∀ (x : X), ¬P x
⊢ ∃ (x : X), P x
X : Type,
P : X → Prop,
h : ¬∀ (x : X), ¬P x
⊢ (¬∃ (x : X), P x) → false
push_neg, contradiction
X : Type,
P : X → Prop,
h : ¬∀ (x : X), ¬P x
⊢ (¬∃ (x : X), P x) → false
X : Type,
P : X → Prop,
h : ¬∀ (x : X), ¬P x
⊢ (∀ (x : X), ¬P x) → false
},
X : Type,
P : X → Prop,
h : ¬∀ (x : X), ¬P x
⊢ (∀ (x : X), ¬P x) → false
X : Type,
P : X → Prop
⊢ (∃ (x : X), P x) → (¬∀ (x : X), ¬P x)
{rintro ⟨x, hx⟩ h,
X : Type,
P : X → Prop
⊢ (∃ (x : X), P x) → (¬∀ (x : X), ¬P x)
X : Type,
P : X → Prop,
h : ∀ (x : X), ¬P x,
x : X,
hx : P x
⊢ false
from (h x) hx
X : Type,
P : X → Prop,
h : ∀ (x : X), ¬P x,
x : X,
hx : P x
⊢ false
X : Type,
P : X → Prop,
h : ∀ (x : X), ¬P x,
x : X,
hx : P x
⊢ false
}
X : Type,
P : X → Prop,
h : ∀ (x : X), ¬P x,
x : X,
hx : P x
⊢ false
no goals