Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-07 17:43 5aa65d6d

View on Github →

order(filter): rename vmap to comap

Estimated changes

Modified analysis/metric_space.lean

added theorem nhds_comap_dist

deleted theorem nhds_vmap_dist

Modified analysis/nnreal.lean

Modified analysis/real.lean

Modified analysis/topology/continuity.lean

added theorem dense_embedding.comap_nhds_neq_bot

added theorem dense_embedding.tendsto_comap_nhds_nhds

deleted theorem dense_embedding.tendsto_vmap_nhds_nhds

deleted theorem dense_embedding.vmap_nhds_neq_bot

added theorem nhds_induced_eq_comap

deleted theorem nhds_induced_eq_vmap

added theorem nhds_subtype_eq_comap

deleted theorem nhds_subtype_eq_vmap

Modified analysis/topology/infinite_sum.lean

Modified analysis/topology/topological_space.lean

Modified analysis/topology/topological_structures.lean

modified theorem filter.map_neg

Modified analysis/topology/uniform_space.lean

added theorem cauchy_comap

deleted theorem cauchy_vmap

added theorem comap_quotient_eq_uniformity

added theorem comap_quotient_le_uniformity

modified theorem eq_of_separated_of_uniform_continuous

added theorem nhds_eq_comap_uniformity

deleted theorem nhds_eq_vmap_uniformity

modified theorem separated_of_uniform_continuous

added theorem to_topological_space_comap

deleted theorem to_topological_space_vmap

modified theorem uniform_continuous.prod_mk

added theorem uniform_continuous_comap'

added theorem uniform_continuous_comap

deleted theorem uniform_continuous_vmap'

deleted theorem uniform_continuous_vmap

added def uniform_space.comap

deleted def uniform_space.vmap

deleted theorem vmap_quotient_eq_uniformity

deleted theorem vmap_quotient_le_uniformity

Modified data/analysis/filter.lean

Modified order/filter.lean

added def filter.comap

added theorem filter.comap_bot

added theorem filter.comap_comap_comp

added theorem filter.comap_eq_lift'

added theorem filter.comap_eq_of_inverse

added theorem filter.comap_id

added theorem filter.comap_inf

added theorem filter.comap_infi

added theorem filter.comap_lift'_eq2

added theorem filter.comap_lift'_eq

added theorem filter.comap_lift_eq2

added theorem filter.comap_lift_eq

added theorem filter.comap_map

added theorem filter.comap_mono

added theorem filter.comap_neq_bot

added theorem filter.comap_neq_bot_of_surj

added theorem filter.comap_principal

added theorem filter.comap_sup

added theorem filter.comap_top

added theorem filter.gc_map_comap

deleted theorem filter.gc_map_vmap

added theorem filter.le_comap_map

added theorem filter.le_map_comap'

added theorem filter.le_map_comap

deleted theorem filter.le_map_vmap'

deleted theorem filter.le_map_vmap

deleted theorem filter.le_vmap_map

modified theorem filter.map_bot

added theorem filter.map_comap_le

added theorem filter.map_eq_comap_of_inverse

deleted theorem filter.map_eq_vmap_of_inverse

added theorem filter.map_le_iff_le_comap

deleted theorem filter.map_le_iff_le_vmap

modified theorem filter.map_mono

modified theorem filter.map_sup

added theorem filter.map_swap_eq_comap_swap

deleted theorem filter.map_swap_eq_vmap_swap

deleted theorem filter.map_vmap_le

added theorem filter.mem_comap_sets

deleted theorem filter.mem_vmap_sets

added theorem filter.monotone_comap

deleted theorem filter.monotone_vmap

added theorem filter.preimage_mem_comap

deleted theorem filter.preimage_mem_vmap

added theorem filter.prod_comap_comap_eq

modified theorem filter.prod_comm'

deleted theorem filter.prod_vmap_vmap_eq

added theorem filter.sInter_comap_sets

deleted theorem filter.sInter_vmap_sets

added theorem filter.tendsto_comap''

added theorem filter.tendsto_comap

added theorem filter.tendsto_comap_iff

added theorem filter.tendsto_iff_comap

deleted theorem filter.tendsto_iff_vmap

deleted theorem filter.tendsto_vmap''

deleted theorem filter.tendsto_vmap

deleted theorem filter.tendsto_vmap_iff

deleted def filter.vmap

deleted theorem filter.vmap_bot

deleted theorem filter.vmap_eq_lift'

deleted theorem filter.vmap_eq_of_inverse

deleted theorem filter.vmap_id

deleted theorem filter.vmap_inf

deleted theorem filter.vmap_infi

deleted theorem filter.vmap_lift'_eq2

deleted theorem filter.vmap_lift'_eq

deleted theorem filter.vmap_lift_eq2

deleted theorem filter.vmap_lift_eq

deleted theorem filter.vmap_map

deleted theorem filter.vmap_mono

deleted theorem filter.vmap_neq_bot

deleted theorem filter.vmap_neq_bot_of_surj

deleted theorem filter.vmap_principal

deleted theorem filter.vmap_sup

deleted theorem filter.vmap_top

deleted theorem filter.vmap_vmap_comp