Zulip Chat Archive

Stream: maths

Topic: contrapositive

ndroock1 (May 19 2022 at 08:19):

As a newbie trying to learn Lean I tried proving the 'Contrapositive' using
example : (P Q : Prop) : (P → Q) -> (¬Q → ¬P) :=
the result was a bunch of errors; what is wrong here ?

ndroock1 (May 19 2022 at 08:20):

STOP: I just saw an error. :-(

ndroock1 (May 19 2022 at 08:23):

Changed it to :
example : (P Q : Prop) : (P → Q) ↔ (¬Q → ¬P) :=
but still errors ...

Alex J. Best (May 19 2022 at 08:23):

You have too many :, there doesn't need to be one after example only after the arguments.

ndroock1 (May 19 2022 at 08:23):

Thx. Will try.

Alex J. Best (May 19 2022 at 08:23):

I.e.

example (P Q : Prop) : (P → Q) ↔ (¬Q → ¬P) :=

Last updated: Dec 20 2023 at 11:08 UTC