Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-26 15:11 ef62d1c0

View on Github →

chore(*): last preparations for Heine (#3179) This is hopefully the last preparatory PR before we study compact uniform spaces. It has almost no mathematical content, except that I define uniform_continuous_on, and check it is equivalent to uniform continuity for the induced uniformity.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.diagonal_eq_range

added theorem set.mem_diagonal

Modified src/order/complete_lattice.lean

added theorem infi_split

added theorem infi_split_single

added theorem supr_split

added theorem supr_split_single

Modified src/order/filter/basic.lean

added theorem filter.comap_const_of_mem

added theorem filter.comap_const_of_not_mem

added theorem filter.comap_prod

added theorem filter.le_iff_forall_inf_principal_compl

added theorem filter.mem_iff_inf_principal_compl

added theorem filter.principal_le_iff

added theorem filter.subtype_coe_map_comap_prod

Modified src/topology/basic.lean

added theorem cluster_pt.of_inf_left

added theorem cluster_pt.of_inf_right

added theorem cluster_pt_iff

deleted theorem cluster_pt_of_inf_left

deleted theorem cluster_pt_of_inf_right

added theorem mem_closure_iff_cluster_pt

added theorem subset_interior_iff_nhds

Modified src/topology/metric_space/basic.lean

added theorem metric.uniform_continuous_on_iff

Modified src/topology/separation.lean

added theorem disjoint_nested_nhds

Modified src/topology/subset_properties.lean

Modified src/topology/uniform_space/basic.lean

added theorem nhds_eq_comap_uniformity_aux

added theorem nhds_le_uniformity

added def uniform_continuous_on

added theorem uniform_continuous_on_iff_restrict

Modified src/topology/uniform_space/separation.lean

modified theorem eq_of_uniformity_inf_nhds