Commit 2023-01-25 19:53 11d5cd71

View on Github →

Feat: add lemmas about Set.diagonal (#1438) This is a partial forward-port of leanprover-community/mathlib#18111

Estimated changes

Modified Mathlib/Data/Set/Function.lean

added theorem Set.mapsTo_prod_map_diagonal

Modified Mathlib/Data/Set/Prod.lean

added theorem Set.diagonal_nonempty

added theorem Set.diagonal_subset_iff

Modified Mathlib/Order/Filter/Bases.lean

deleted theorem Filter.HasBasis.comp_of_surjective

added theorem Filter.HasBasis.comp_surjective

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.comap_id'

added theorem Filter.mem_comap_prod_mk