title: Convergence and vectors theories
body: <p>Is there a convergence theory in Isabelle/HOL? I need to define <code>∥x(t)∥ ⟶ 0 as t ⟶ ∞</code>. </p>
  
  <p>Also, I'm looking for vectors theory, I found a matrix theory but I couldn't find the vectors one, Is there exist such theory in Isabelle/HOL?</p>
  
  <p>Cheers.  </p>