syntax question about lambda

Stream: new members

[Marcus Rossel]

Yes, Lean uses the syntax λ x : α, <expression using x> to denote a function that maps all x (of type α in this case) to some value that can depend on x.
Assuming f to be a function of type α -> α, the expression f (f x) will also be of type α. So your entire lambda expression ends up being a function of type α -> α.