Commit 2020-10-13 21:59 2543b688

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

Lemmas

• 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;

Definitions

• unique_diff_within_at;
• residual;

Rename

• submodule.linear_eq_on → linear_map.eq_on_span, linear_map.eq_on_span';
• submodule.linear_map.ext_on → linear_map.ext_on_range;
• filter.is_countably_generated.has_antimono_basis → filter.is_countably_generated.exists_antimono_basis;
• exists_countable_closure_eq_univ → exists_countable_dense, use dense;
• dense_seq_dense → dense_range_dense_seq, use dense;
• dense_range.separable_space is now protected;
• dense_of_subset_dense → dense.mono;
• dense_inter_of_open_left → dense.inter_of_open_left;
• dense_inter_of_open_right → dense.inter_of_open_right;
• continuous.dense_image_of_dense_range → dense_range.dense_image;
• dense_range.inhabited, dense_range.nonempty: changed API, TODO;
• quotient_dense_of_dense → dense.quotient, use dense;
• dense_inducing.separable → dense_inducing.separable_space, add protected;
• dense_embedding.separable → dense_embedding.separable_space, add protected;
• dense_inter_of_Gδ → dense.inter_of_Gδ;
• stone_cech_unit_dense → dense_range_stone_cech_unit;
• abstract_completion.dense' → abstract_completion.closure_range;
• Cauchy.pure_cauchy_dense → Cauchy.dense_range_pure_cauchy;
• completion.dense → completion.dense_range_coe;
• completion.dense₂ → completion.dense_range_coe₂;
• completion.dense₃ → completion.dense_range_coe₃;

New

• 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 dense_closure.mp and dense_closure.mpr;
• dense_univ: univ is dense;
• dense.inter_open_nonempty: alias for dense_iff_inter_open.mp;
• 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;
• dense.prod: product of two dense sets is dense in the product;
• set.eq_on.closure;
• continuous.ext_on;
• linear_map.ext_on