Problem with defining theorem due to types

Stream: new members

[Labyrinth]

Hi, newbie here.

Sorry for the undescriptive title, but I couldn't think of what to put there without a 50/50 chance of it being wrong.

I have the following code:

import Mathlib

def seq_limit (u : ℕ → ℝ) (l : ℝ) :=
  ∀ε > 0, ∃N : ℕ, ∀n > N, |u n - l| < ε

theorem seq_limit_bound_of_bound (seq_limit u l) (h : ∀n, u n ≤ M) :
  l ≤ M := by

And I get this error message:

Function expected at
  u
but this term has type
  ?m.3

Note: Expected a function because this term is being applied to the argument
  n

On top of that, only M is automatically added as an implicit parameter. Shouldn't u and l also be, since I never added them as arguments or variables anywhere? And why doesn't it attribute u's type to that of the first argument of seq_limit?

[Kenny Lau]

it's (hl : seq_limit u l)