[Merged by Bors] - chore(*): golf #18111
Closed
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Sets
set.maps_to_prod_map_diagonal
,set.diagonal_nonempty
, andset.diagonal_subset_iff
.Filters
nhds_eq_comap_uniformity_aux
tofilter.mem_comap_prod_mk
.set.nonempty.principal_ne_bot
andfilter.comap_id'
.filter.has_basis.comp_of_surjective
tofilter.has_basis.comp_surjective
.Uniform spaces
monotone_comp_rel
tomonotone.comp_rel
to enable dot notation.nhds_eq_comap_uniformity'
.𝓝ˢ (diagonal γ)
instead of⨆ x, 𝓝 (x, x)
inuniform_space_of_compact_t2
.Mathlib 4 port
Relevant parts are forward-ported in leanprover-community/mathlib4#1438