The absorbing law

Stream: lean4

[loooong]

I'm learning lean4 by mathematics in lean. In the sec 2.5 page 21, I notice that the left hand side of the second absorbing law is x \lub x \glb y but not x \lub (x \glb y). whiy these brakets can be ignored?

[Kevin Buzzard]

\lub and \glb are notation, and the way notation works in Lean is that it has a "binding power". To give a familiar example: the binding power of * is larger than the binding power of +, so a + b * c gets parsed as a + (b * c), whereas a * b + c gets parsed as (a * b) + c. To figure out why the brackets can be ignored you will need to know the binding power of \lub and \glb. In Lean 3 this was easily established using #print notation but I'm not sure what the lean 4 equivalent is. However one can still ctrl-click on the notation which takes you to the definitions of the symbols in mathlib:

@[inherit_doc]
infixl:68 " ⊔ " => Sup.sup

@[inherit_doc]
infixl:69 " ⊓ " => Inf.inf

So \glb has a slightly higher binding power than \lub (69 > 68) meaning that the brackets aren't needed.

[Kevin Buzzard]

I would be interested in knowing if there is a trick to discover the binding power of the notation in Lean 4 without jumping to its definition.

[loooong]

thank you @Kevin Buzzard . :+1: