Theorem Nat.exists_strictMono_subsequence

Modification history

2025-04-23 04:28
Mathlib/Order/Monotone/Basic.lean
chore (Order/Monotone/Basic): move/rename subsequence existence lemma (#24207) …
Added Nat.exists_strictMono_subsequenceView on Github →