Commit 2023-01-25 11:06 f974ae84

chore(*): golf (#18111)

Sets

• Add set.maps_to_prod_map_diagonal, set.diagonal_nonempty, and set.diagonal_subset_iff.

Filters

• Generalize and rename nhds_eq_comap_uniformity_aux to filter.mem_comap_prod_mk.
• Add set.nonempty.principal_ne_bot and filter.comap_id'.
• Rename filter.has_basis.comp_of_surjective to filter.has_basis.comp_surjective.

Uniform spaces

• Rename monotone_comp_rel to monotone.comp_rel to enable dot notation.
• Add nhds_eq_comap_uniformity'.
• Use 𝓝ˢ (diagonal γ) instead of ⨆ x, 𝓝 (x, x) in uniform_space_of_compact_t2.
• Golf here and there.

Mathlib 4 port

Relevant parts are forward-ported in leanprover-community/mathlib4#1438