docs(order/order_iso_nat): Added note on `exists_increasing_or_noninc…

…reasing_subseq` (#12239)
leanprover-community · Feb 23, 2022 · 3e2df83 · 3e2df83
1 parent 162d060
commit 3e2df83
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/order/order_iso_nat.lean b/src/order/order_iso_nat.lean
@@ -140,6 +140,8 @@ begin
       or.intro_left _ (λ n, (nat.find_spec (h (g' n))).2)⟩ }
 end
 
+/-- This is the infinitary Erdős–Szekeres theorem, and an important lemma in the usual proof of
+    Bolzano-Weierstrass for `ℝ`. -/
 theorem exists_increasing_or_nonincreasing_subseq
   {α : Type*} (r : α → α → Prop) [is_trans α r] (f : ℕ → α) :
   ∃ (g : ℕ ↪o ℕ), (∀ m n : ℕ, m < n → r (f (g m)) (f (g n))) ∨