Commit 2026-11-10 23:16 a1ba21c8

View on Github →

feat(Combinatorics/SimpleGraph/Maps): more map/comap API (#42370)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.coe_equivOfBijective

added theorem SimpleGraph.coe_symm_equivOfBijective

added theorem SimpleGraph.comap_bijective

added theorem SimpleGraph.comap_injective

added theorem SimpleGraph.comap_le_of_le_map

added theorem SimpleGraph.edgeSet_comap

added theorem SimpleGraph.edgeSet_induce

added def SimpleGraph.equivOfBijective

added theorem SimpleGraph.equivOfBijective_id

added theorem SimpleGraph.equivOfBijective_trans

added theorem SimpleGraph.le_map_iff_comap_le

added theorem SimpleGraph.le_map_of_comap_le

added theorem SimpleGraph.le_spanningCoe_top_coe

added theorem SimpleGraph.leftInverse_map_comap

added theorem SimpleGraph.map_bijective

added theorem SimpleGraph.map_comap_eq

added theorem SimpleGraph.map_comap_eq_inf

modified theorem SimpleGraph.map_comap_le

added theorem SimpleGraph.map_surjective

added theorem SimpleGraph.map_top

added theorem SimpleGraph.spanningCoe_induce_eq_inf

modified theorem SimpleGraph.spanningCoe_induce_eq_self