Commit 2023-02-05 12:15 d62493a6

View on Github →

feat: port Order.Filter.Partial (#2059)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Partial.lean

added def Filter.Ptendsto'

added def Filter.Ptendsto

added def Filter.Rtendsto'

added def Filter.Rtendsto

added theorem Filter.mem_pmap

added theorem Filter.mem_rcomap'

added theorem Filter.mem_rmap

added def Filter.pcomap'

added def Filter.pmap

added theorem Filter.pmap_res

added theorem Filter.ptendsto'_def

added theorem Filter.ptendsto'_of_ptendsto

added theorem Filter.ptendsto_def

added theorem Filter.ptendsto_iff_rtendsto

added theorem Filter.ptendsto_of_ptendsto'

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 theorem Filter.rtendsto'_def

added theorem Filter.rtendsto_def

added theorem Filter.rtendsto_iff_le_rcomap

added theorem Filter.tendsto_iff_ptendsto

added theorem Filter.tendsto_iff_ptendsto_univ

added theorem Filter.tendsto_iff_rtendsto'

added theorem Filter.tendsto_iff_rtendsto