Theorem Filter.extraction_of_frequently_atTop'

Modification history

2025-04-23 04:28

Mathlib/Order/Filter/AtTopBot/Basic.lean

chore (Order/Monotone/Basic): move/rename subsequence existence lemma (#24207) …

Deleted Filter.extraction_of_frequently_atTop'View on Github →

2025-02-10 19:23

Mathlib/Order/Filter/AtTopBot.lean

chore(Order/Filter): split `AtTopBot.lean` (#21672) …

Modified Filter.extraction_of_frequently_atTop'View on Github →

2023-01-24 09:14

Mathlib/Order/Filter/AtTopBot.lean

feat: port Order.Filter.AtTopBot (#1795)

Added Filter.extraction_of_frequently_atTop'View on Github →