Zulip Chat Archive

Stream: new members

Topic: brackets vs parentheses vs none


Holly Liu (Jun 16 2021 at 03:08):

hi again :). i have a question about this code:

import data.set
open set

variable {U : Type}
variables A B C : set U
variable x : U

#check x  A

if we're trying to prove something about an element of a set rather than the set itself, how do we do that in lean? i was trying to declare it as a variable but am stuck.
when declaring variables, when should we use {} versus no brackets? does variable (x : U) ever happen? i also see this here (from the tutorials project):

example (a b : ): 0  b  a  a + b :=
example {a b : } : (0  a  0  b)  0  a + b :=

i'm unsure of the difference here.

Heather Macbeth (Jun 16 2021 at 03:09):

You can write, say,

variable (h : x  A)

Is that what you're after?

Mario Carneiro (Jun 16 2021 at 03:10):

No brackets is equivalent to round brackets. I prefer the round bracket form because no brackets does not work in most places

Mario Carneiro (Jun 16 2021 at 03:12):

also round brackets is shorter since you can write variables (t : T) (u : U) instead of variables t : T variables u : U

Holly Liu (Jun 16 2021 at 03:12):

You can write, say,

variable (h : x  A)

Is that what you're after?

oh yeah i think that's what i'm looking for. so h would be an element of A?

Mario Carneiro (Jun 16 2021 at 03:12):

h is a proof that x is in A

Holly Liu (Jun 16 2021 at 03:12):

oh ok

Mario Carneiro (Jun 16 2021 at 03:13):

an "element of A" (where A : set U) is a pair of an element of U and a proof that that element is in A

Holly Liu (Jun 16 2021 at 03:19):

oh ok, so could we do something like example (h : x \in A) (j : x \in B) : h \neq j :=(this might be mathematically incorrect) where \neq means not equal

Mario Carneiro (Jun 16 2021 at 03:22):

that's not type correct, h and j don't have the same type so they can't be equated

Holly Liu (Jun 16 2021 at 03:26):

ah i see

Holly Liu (Jun 16 2021 at 03:31):

also, is there a difference when using brackets vs parentheses?

Mario Carneiro (Jun 16 2021 at 03:39):

Yes, brackets means that the variable should be inferred by type class inference

Mario Carneiro (Jun 16 2021 at 03:40):

see https://leanprover.github.io/theorem_proving_in_lean/type_classes.html

Holly Liu (Jun 16 2021 at 04:00):

ok, thanks!


Last updated: Dec 20 2023 at 11:08 UTC