From 490c472d223b9b3e914ba6717fdd1e5ba464d362 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Mon, 29 Jun 2026 08:59:51 -0500
Subject: [PATCH] Start documenting FiniteMap.lean

---
 lean/Spa/Lattice/FiniteMap.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/lean/Spa/Lattice/FiniteMap.lean b/lean/Spa/Lattice/FiniteMap.lean
index ff82edf..16c3af8 100644
--- a/lean/Spa/Lattice/FiniteMap.lean
+++ b/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