Commit 2020-10-13 21:59 2543b688

View on Github →

refactor(*): migrate to dense API (#4447) @PatrickMassot introduced dense in #4399. In this PR I review the API and migrate many definitions and lemmas to use dense s instead of closure s = univ. I also generalize second_countable_of_separable to a uniform_space with a countably generated uniformity filter.

API changes

Use dense or dense_range instead of closure _ = univ


  • has_fderiv_within_at.unique_diff_within_at;
  • exists_dense_seq;
  • dense_Inter_of_open_nat;
  • dense_sInter_of_open;
  • dense_bInter_of_open;
  • dense_Inter_of_open;
  • dense_sInter_of_Gδ;
  • dense_bInter_of_Gδ;
  • eventually_residual;
  • mem_residual;
  • dense_bUnion_interior_of_closed;
  • dense_sUnion_interior_of_closed;
  • dense_Union_interior_of_closed;
  • Kuratowski_embeddinng.embedding_of_subset_isometry;
  • continuous_extend_from;


  • unique_diff_within_at;
  • residual;


  • submodule.linear_eq_onlinear_map.eq_on_span, linear_map.eq_on_span';
  • submodule.linear_map.ext_onlinear_map.ext_on_range;
  • filter.is_countably_generated.has_antimono_basisfilter.is_countably_generated.exists_antimono_basis;
  • exists_countable_closure_eq_univexists_countable_dense, use dense;
  • dense_seq_densedense_range_dense_seq, use dense;
  • dense_range.separable_space is now protected;
  • dense_of_subset_densedense.mono;
  • dense_inter_of_open_leftdense.inter_of_open_left;
  • dense_inter_of_open_rightdense.inter_of_open_right;
  • continuous.dense_image_of_dense_rangedense_range.dense_image;
  • dense_range.inhabited, dense_range.nonempty: changed API, TODO;
  • quotient_dense_of_densedense.quotient, use dense;
  • dense_inducing.separabledense_inducing.separable_space, add protected;
  • dense_embedding.separabledense_embedding.separable_space, add protected;
  • dense_inter_of_Gδdense.inter_of_Gδ;
  • stone_cech_unit_densedense_range_stone_cech_unit;
  • abstract_completion.dense'abstract_completion.closure_range;
  • Cauchy.pure_cauchy_denseCauchy.dense_range_pure_cauchy;
  • completion.densecompletion.dense_range_coe;
  • completion.dense₂completion.dense_range_coe₂;
  • completion.dense₃completion.dense_range_coe₃;


  • has_fderiv_within_at.unique_on : if f' and f₁' are two derivatives of f within s at x, then they are equal on the tangent cone to s at x;
  • local_homeomorph.mdifferentiable.mfderiv_bijective, local_homeomorph.mdifferentiable.mfderiv_surjective
  • continuous_linear_map.eq_on_closure_span: if two continuous linear maps are equal on s, then they are equal on closure (submodule.span s);
  • continuous_linear_map.ext_on: if two continuous linear maps are equal on a set s such that submodule.span s is dense, then they are equal;
  • dense_closure: closure s is dense iff s is dense;
  • dense.of_closure, dense.closure: aliases for and dense_closure.mpr;
  • dense_univ: univ is dense;
  • dense.inter_open_nonempty: alias for;
  • dense.nonempty_iff: if s : set α is a dense set, then s is nonempty iff α is nonempty;
  • dense.nonempty: a dense set in a nonempty type is nonempty;
  • dense_range.some: given a function with dense_range and a point in the codomain, returns a point in the domain;
  • function.surjective.dense_range: a surjective function has dense range;
  • continuous.range_subset_closure_image_dense: closure of the image of a dense set under a continuous function includes the range of this function;
  • dense_range.dense_of_maps_to: if a function with dense range maps a dense set s to t, then t is dense in the codomain;
  • dense_range.quotient;
  • product of two dense sets is dense in the product;
  • set.eq_on.closure;
  • continuous.ext_on;
  • linear_map.ext_on

Estimated changes