Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-15 13:35 73586053

View on Github →

feat(analysis/topology/completion): comm_ring on separation quotient, completion (separation_quotient A) is equivalent to completion A

Estimated changes

Modified analysis/topology/completion.lean

deleted theorem filter.prod_pure_pure

deleted theorem uniform_space.cauchy_prod

deleted theorem uniform_space.complete_space_separation

added def uniform_space.completion.completion_separation_quotient_equiv

added theorem uniform_space.completion.ext

added theorem uniform_space.completion.extension_map

added theorem uniform_space.completion.map_comp

added theorem uniform_space.completion.map_id

added theorem uniform_space.completion.map_unique

added theorem uniform_space.completion.uniform_continuous_completion_separation_quotient_equiv

added theorem uniform_space.completion.uniform_continuous_completion_separation_quotient_equiv_symm

deleted theorem uniform_space.separated_separation

added def uniform_space.separation_quotient.lift

added theorem uniform_space.separation_quotient.lift_mk

added def uniform_space.separation_quotient.map

added theorem uniform_space.separation_quotient.map_comp

added theorem uniform_space.separation_quotient.map_id

added theorem uniform_space.separation_quotient.map_mk

added theorem uniform_space.separation_quotient.map_unique

added theorem uniform_space.separation_quotient.uniform_continuous_lift

added theorem uniform_space.separation_quotient.uniform_continuous_map

added def uniform_space.separation_quotient

deleted theorem uniform_space.uniform_continuous_of_const

Modified analysis/topology/continuity.lean

added theorem mem_closure2

added theorem mem_closure

Modified analysis/topology/topological_structures.lean

deleted theorem is_ideal_iff

Modified data/quot.lean

added theorem nonempty_quotient_iff

Modified data/set/basic.lean

deleted theorem set.image_subset_iff'

Modified order/filter.lean

added theorem filter.prod_pure_pure