diff --git a/src/order/lexicographic.lean b/src/order/lexicographic.lean
index 6271b820a0096..1bcd573a9b3ba 100644
--- a/src/order/lexicographic.lean
+++ b/src/order/lexicographic.lean
@@ -10,6 +10,7 @@ import tactic.basic
 
 universes u v
 
+/-- The cartesian product, equipped with the lexicographic order. -/
 def lex (α : Type u) (β : Type v) := α × β
 
 variables {α : Type u} {β : Type v}
diff --git a/src/order/pilex.lean b/src/order/pilex.lean
index aa44fa40efd67..57310b701b941 100644
--- a/src/order/pilex.lean
+++ b/src/order/pilex.lean
@@ -10,9 +10,12 @@ import algebra.order_functions
 variables {ι : Type*} {β : ι → Type*} (r : ι → ι → Prop)
   (s : Π {i}, β i → β i → Prop)
 
+/-- The lexicographic relation on `Π i : ι, β i`, where `ι` is ordered by `r`,
+  and each `β i` is ordered by `s`. -/
 def pi.lex (x y : Π i, β i) : Prop :=
 ∃ i, (∀ j, r j i → x j = y j) ∧ s (x i) (y i)
 
+/-- The cartesian product of an indexed family, equipped with the lexicographic order. -/
 def pilex (α : Type*) (β : α → Type*) : Type* := Π a, β a
 
 instance [has_lt ι] [∀ a, has_lt (β a)] : has_lt (pilex ι β) :=