Mathlib Changelog
v3
Changelog
About
Github
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