Commit 2026-09-05 23:16 29ea5de9

View on Github →

feat(Combinatorics/SimpleGraph/Maps): (f : H →g G) → H.map f ≤ G (#43347) Matches Hom.le_comap

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.Hom.map_le

modified theorem SimpleGraph.map_le_iff_le_comap

added theorem SimpleGraph.map_le_of_le_comap