What does the leading turnstile operator mean?

I know that different authors use different notation to represent programming language semantics. As a matter of fact Guy Steele addresses this problem in an interesting video.

I'd like to know if anyone knows whether the leading turnstile operator has a well recognized meaning. For example I don't understand the leading $\vdash$ operator at the beginning of the denominator of the following:

$$\frac{x:T_1 \vdash t_2:T_2}{\vdash \lambda x:T_1 . t_2 ~:~ T_1 \to T_2}$$

Can someone help me understand?
Thanks.

On the left of the turnstile, you can find the local context, a finite list of assumptions on the types of the variables at hand.

$$
x_1:T_1, \ldots, x_n:T_n \vdash e:T
$$

Above, $n$ can be zero, resulting in $\vdash e:T$. This means that no assumptions on variables are made. Usually, this means that $e$ is a closed term (without any free variables) having type $T$.

Often, the rule you mention is written in a more general form, where there can be more hypotheses than the one mentioned in the question.

$$
\dfrac{
\Gamma, x:T_1 \vdash t : T_2
}{
\Gamma\vdash (\lambda x:T_1. t) : T_1\to T_2
}
$$

Here, $\Gamma$ represents any context, and $\Gamma, x:T_1$ represents its extension obtained by appending the additional hypothesis $x:T_1$ to the list $\Gamma$. It is common to require that $x$ did not appear in $\Gamma$, so that the extension does not "conflict" with a previous assumption.

StackExchange Computer Science Q#97442, answer score: 19