Jordan Kloosterman

Stream: new members

[Jordan Kloosterman]

Hi everyone,

My name's Jordan and I'm new. I've graduated college in computer science (made a math club while I was there) and I'm currently learning Lean and proofs and hoping to go to University this winter.

I was going through the Mathematics in Lean book and I have a question from this section (section 2.3)(hopefully asking here is ok)
https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html#using-theorems-and-lemmas

why is it:
#check (le_trans : a ≤ b → b ≤ c → a ≤ c) -- a ≤ b implies b ≤ c implies a ≤ c

instead of:
#check (le_trans : a ≤ b ∧ b ≤ c → a ≤ c)-- a ≤ b and b ≤ c implies a ≤ c

[Aaron Liu]

Jordan Kloosterman said:

why is it:
#check (le_trans : a ≤ b → b ≤ c → a ≤ c) -- a ≤ b implies b ≤ c implies a ≤ c

instead of:
#check (le_trans : a ≤ b ∧ b ≤ c → a ≤ c)-- a ≤ b and b ≤ c implies a ≤ c

When you're using the theorem and you have hab : a ≤ b and hbc : b ≤ c it's easier to write le_trans hab hbc than le_trans (And.intro hab hbc) or le_trans ⟨hab, hbc⟩

[Aaron Liu]

so most of the theorems are curried

[Jordan Kloosterman]

curried?

[Aaron Liu]

https://en.wikipedia.org/wiki/Currying#Logic

[Jordan Kloosterman]

Ok, so it's to make it easier to put in the lambda function arguments right?

I'm just a bit confused by the notation, does the right arrow mean implies here? or is it not working like that? cause with the first to me it looks like you'd be able to conclude that b ≤ c from just a ≤ b

[Aaron Liu]

it's a ≤ b → (b ≤ c → a ≤ c)

[Aaron Liu]

so if you have that a ≤ b you can conclude that b ≤ c → a ≤ c

[Jordan Kloosterman]

ok, that makes a lot more sense, thank you