Commit 2025-04-23 04:28 b5a7ec88

View on Github →

chore (Order/Monotone/Basic): move/rename subsequence existence lemma (#24207) I'd like to use this lemma without importing filters.

Estimated changes

Modified Mathlib/Order/Filter/AtTopBot/Basic.lean

deleted theorem Filter.extraction_of_frequently_atTop'

Modified Mathlib/Order/Monotone/Basic.lean

added theorem Nat.exists_strictMono_subsequence

Modified scripts/nolints_prime_decls.txt