Start documenting FiniteMap.lean

lean/Spa/Lattice/FiniteMap.lean

@@ -1,8 +1,23 @@
 import Spa.Lattice.Tuple
 import Mathlib.Data.List.Nodup
 
+/-!
+
+# Finite Maps
+
+This file defines _finite maps_, or key-value maps with a finite domain. This
+is encoded as a map from `Fin` into the value type. Finite maps form a
+lattice from pointwise composition: $(f \land g) k = f k \land g k$,
+and, provided the domain `\beta` is of finite height, so is the map
+lattice as a whole.
+
+In fact, the isomorphism is described and proven in `Spa/Lattice/Tuple.lean`.
+
+-/
+
 namespace Spa
 
+/-- Key-value map with domain `α` and codomain `β`, with possible keys $\textit{ks} \subseteq \alpha$. -/
 def FiniteMap (α β : Type*) (ks : List α) : Type _ := Fin ks.length → β
 
 namespace FiniteMap