  LaSalle invariance principle was originally proposed in the 1950's and has
become a fundamental mathematical tool in the area of dynamical systems and
control. In both theoretical research and engineering practice, discrete-time
dynamical systems have been at least as extensively studied as continuous-time
systems. For example, model predictive control is typically studied in
discrete-time via Lyapunov methods. However, there is a peculiar absence in the
standard literature of standard treatments of Lyapunov functions and LaSalle
invariance principle for discrete-time nonlinear systems. Most of the textbooks
on nonlinear dynamical systems focus only on continuous-time systems. In
Chapter 1 of the book by LaSalle [11], the author establishes the LaSalle
invariance principle for difference equation systems. However, all the useful
lemmas in [11] are given in the form of exercises with no proof provided. In
this document, we provide the proofs of all the lemmas proposed in [11] that
are needed to derive the main theorem on the LaSalle invariance principle for
discrete-time dynamical systems. We organize all the materials in a
self-contained manner. We first introduce some basic concepts and definitions
in Section 1, such as dynamical systems, invariant sets, and limit sets. In
Section 2 we present and prove some useful lemmas on the properties of
invariant sets and limit sets. Finally, we establish the original LaSalle
invariance principle for discrete-time dynamical systems and a simple extension
in Section~3. In Section 4, we provide some references on extensions of LaSalle
invariance principles for further reading. This document is intended for
educational and tutorial purposes and contains lemmas that might be useful as a
reference for researchers.
