Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-08 09:28 a96fa3be

View on Github →

feat(order/filter): convergence for relations and partial functions

Estimated changes

Modified src/data/pfun.lean

modified def pfun.core

modified def pfun.graph'

modified theorem pfun.mem_core

modified theorem pfun.mem_core_res

modified theorem pfun.preimage_as_subtype

modified theorem roption.mem_restrict

Renamed data/rel.lean to src/data/rel.lean

Modified src/order/filter.lean

added theorem filter.le_map_comap_of_surjective'

added theorem filter.le_map_comap_of_surjective

added theorem filter.map_comap_of_surjective'

added theorem filter.map_comap_of_surjective

added theorem filter.mem_inf_principal

added def filter.mem_pmap

added def filter.mem_rcomap'

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 theorem filter.ptendsto'_of_ptendsto

added def filter.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 def filter.rtendsto'

added theorem filter.rtendsto'_def

added def filter.rtendsto

added theorem filter.rtendsto_def

added theorem filter.rtendsto_iff_le_comap

added theorem filter.tendsto_if

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