Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-02 10:12 dcd0466d

View on Github →

feat(analysis/topology): complete sets, minor modifications (#557)

Estimated changes

Modified analysis/limits.lean

Modified analysis/metric_space.lean

Modified analysis/normed_space.lean

Modified analysis/topology/infinite_sum.lean

Modified analysis/topology/topological_space.lean

added theorem is_closed_of_closure_subset

modified theorem mem_closure_of_tendsto

added theorem mem_of_closed_of_tendsto'

Modified analysis/topology/topological_structures.lean

deleted theorem Inf_of_Inf_of_monotone_of_continuous

added theorem Inf_of_continuous'

added theorem Inf_of_continuous

deleted theorem Sup_of_Sup_of_monotone_of_continuous

added theorem Sup_of_continuous'

added theorem Sup_of_continuous

added theorem ge_of_tendsto

added theorem infi_of_continuous

deleted theorem infi_of_infi_of_monotone_of_continuous

modified theorem le_of_tendsto

added theorem le_of_tendsto_of_tendsto

added theorem supr_of_continuous

deleted theorem supr_of_supr_of_monotone_of_continuous

Modified analysis/topology/uniform_space.lean

added theorem compact_iff_totally_bounded_complete

deleted theorem compact_of_totally_bounded_complete

deleted theorem complete_of_compact_set

deleted theorem complete_of_is_closed

added theorem complete_space_of_is_complete_univ

added theorem complete_univ

added theorem is_closed_of_is_complete

added def is_complete

added theorem is_complete_image_iff

added theorem is_complete_of_is_closed