# 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`

#### 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`