Commit 2026-04-26 22:04 977f84bd

View on Github →

feat(Combinatorics/SimpleGraph/Maps): characterize neighborSet and edgeSet across an embedding (#35628)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.Embedding.preimage_edgeSet

added theorem SimpleGraph.Embedding.preimage_neighborSet

added theorem SimpleGraph.Hom.image_edgeSet_subset

added theorem SimpleGraph.Hom.image_neighborSet_subset

added theorem SimpleGraph.Hom.subset_preimage_edgeSet

added theorem SimpleGraph.Hom.subset_preimage_neighborSet

added theorem SimpleGraph.Iso.image_neighborSet

added theorem SimpleGraph.map_adj_apply'

added theorem SimpleGraph.neighborSet_comap

added theorem SimpleGraph.neighborSet_induce

added theorem SimpleGraph.neighborSet_map

added theorem SimpleGraph.neighborSet_map_equiv

added theorem SimpleGraph.neighborSet_mono