brackets vs parentheses vs none

Stream: new members

[Holly Liu]

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]

You can write, say,

variable (h : x ∈ A)

Is that what you're after?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Holly Liu]

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]

h is a proof that x is in A

[Holly Liu]

oh ok

[Mario Carneiro]

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]

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]

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

[Holly Liu]

ah i see

[Holly Liu]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Holly Liu]

ok, thanks!