notation in theorem statements

Stream: new members

[Paul Nelson]

Is there a way to introduce notation in the formulation of a theorem? Something like this:

import Mathlib

example
  (x : ℝ)
  (f : ℝ → ℝ)
  let y : ℝ := f x
  : y = y := by sorry

[Richard Copley]

After the colon.

import Mathlib

example
  (x : ℝ)
  (f : ℝ → ℝ) :
  let y : ℝ := f x
  y = y := by sorry

[Paul Nelson]

thanks, this works well if I want to use y in the conclusion. let's suppose I also wanted to use y in some additional hypotheses (e.g., (h : y = 2) appearing before the conclusion). I guess I could just curry those so they appear after the colon, but is there some way to introduce the notation before?

e.g., the first example here works while the second does not, but if there are many hypotheses, doing it as in the first example would get a bit awkward

import Mathlib

example
  (x : ℝ)
  (f : ℝ → ℝ) :
  let y : ℝ := f x
  y = 2 → y = y := by sorry

example
  (x : ℝ)
  (f : ℝ → ℝ)
  let y : ℝ := f x
  (h : y = 2) : y = y := by sorry

[Richard Copley]

No, I think using ∀ and/or → as you suggest is the only way.

[Paul Nelson]

OK, thanks!

[Mario Carneiro]

you can also have a hypothesis (hy : y = f x) which you can put anywhere in the statement