anonymous angle brackets

Stream: new members

[Robert Watson]

I've come across anonymous angle brackets ⟨ and ⟩ in the Tutorials (I'm using Lean 3). What actually are these in terms of types? Is this notation for a sigma type (in the Tutorials it looks more like a Cartesian product)? What actually is the full syntax for these angle brackets - when exactly does one use them? But in the example (below) normal parentheses are used for what I think must be a sigma type, so I'm finding this confusing...

I understand that there are differences between tactics as to how parentheses are used, and then presumably the same again outside tactics mode. So what handle do I need on this to make sense of the different uses?

example {x y : ℝ} : (∀ ε > 0, y ≤ x + ε) →  y ≤ x :=
begin
  contrapose!,
  intro h,
  exact ⟨(y-x)/2, by linarith, by linarith⟩,
end