Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-08 09:28 cfd2b75e

View on Github →

feat(order/filter): break filter into smaller files

Estimated changes

deleted def filter.mem_pmap
deleted def filter.mem_rcomap'
deleted theorem filter.mem_rmap
deleted def filter.pcomap'
deleted def filter.pmap
deleted theorem filter.pmap_res
deleted def filter.ptendsto'
deleted theorem filter.ptendsto'_def
deleted def filter.ptendsto
deleted theorem filter.ptendsto_def
deleted def filter.rcomap'
deleted theorem filter.rcomap'_compose
deleted theorem filter.rcomap'_rcomap'
deleted theorem filter.rcomap'_sets
deleted def filter.rcomap
deleted theorem filter.rcomap_compose
deleted theorem filter.rcomap_rcomap
deleted theorem filter.rcomap_sets
deleted def filter.rmap
deleted theorem filter.rmap_compose
deleted theorem filter.rmap_rmap
deleted theorem filter.rmap_sets
deleted def filter.rtendsto'
deleted theorem filter.rtendsto'_def
deleted def filter.rtendsto
deleted theorem filter.rtendsto_def
added def filter.mem_pmap
added theorem filter.mem_rmap
added def filter.pcomap'
added def filter.pmap
added theorem filter.pmap_res
added def filter.ptendsto'
added theorem filter.ptendsto'_def
added def filter.ptendsto
added theorem filter.ptendsto_def
added def filter.rcomap'
added theorem filter.rcomap'_compose
added theorem filter.rcomap'_rcomap'
added theorem filter.rcomap'_sets
added def filter.rcomap
added theorem filter.rcomap_compose
added theorem filter.rcomap_rcomap
added theorem filter.rcomap_sets
added def filter.rmap
added theorem filter.rmap_compose
added theorem filter.rmap_rmap
added theorem filter.rmap_sets
added def filter.rtendsto'
added theorem filter.rtendsto'_def
added def filter.rtendsto
added theorem filter.rtendsto_def