 <span class="math inline">\(x\)</span> such that <span class="math inline">\(P(x)\)</span>.”</p>
</div>
<p>Lean also uses these symbols, although we will see that quantified statements are written slightly differently in Lean from the way they are written in <em>HTPI</em>. In the statement <span class="math inline">\(P(x)\)</span>, the variable <span class="math inline">\(x\)</span> is called a <em>free variable</em>. But in <span class="math inline">\(\forall x\,P(x)\)</span> or <span class="math inline