Skip to content

[Merged by Bors] - feat(Combinatorics/SimpleGraphs): generalize SimpleGraph.map to any function #36130

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
vbeffara wants to merge 13 commits into from
+39 −31
Closed

[Merged by Bors] - feat(Combinatorics/SimpleGraphs): generalize SimpleGraph.map to any function #36130

Changes from 1 commit
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
f49ee61
Extend SimpleGraph.map to general functions
vbeffara Mar 4, 2026
e6b7cb8
One small generalization
vbeffara Mar 4, 2026
9279ae0
CI build error
vbeffara Mar 4, 2026
4787b14
CI build error
vbeffara Mar 4, 2026
2c5f349
Small updates
vbeffara Mar 4, 2026
eff8ef3
Update Mathlib/Combinatorics/SimpleGraph/Maps.lean
vbeffara Mar 4, 2026
454daf7
Update Mathlib/Combinatorics/SimpleGraph/Maps.lean
vbeffara Mar 4, 2026
4275fd8
Update Mathlib/Combinatorics/SimpleGraph/Maps.lean
vbeffara Mar 4, 2026
bd455c6
Update Mathlib/Combinatorics/SimpleGraph/Maps.lean
vbeffara Mar 4, 2026
d4573a4
Update Mathlib/Combinatorics/SimpleGraph/Maps.lean
vbeffara Mar 4, 2026
ee4dc85
Update Mathlib/Combinatorics/SimpleGraph/Maps.lean
vbeffara Mar 4, 2026
699dc41
Update Mathlib/Combinatorics/SimpleGraph/Clique.lean
vbeffara Mar 4, 2026
04e10ed
Last tweak
vbeffara Mar 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Last tweak
  • Loading branch information
@vbeffara
vbeffara committed Mar 5, 2026
commit 04e10edc45f0975a7569a0ae9899e705555ae0e3
5 changes: 1 addition & 4 deletions Mathlib/Combinatorics/SimpleGraph/Maps.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -595,10 +595,7 @@ lemma comap_symm_apply (f : V ≃ W) (G : SimpleGraph W) (w : W) :

/-- Given a bijective function, there is an isomorphism from a graph into the mapped graph. -/
protected def map (f : V ≃ W) (G : SimpleGraph V) : G ≃g G.map f.toEmbedding :=
{ f with map_rel_iff' := by {
rw [Equiv.coe_toEmbedding]
grind [Equiv.apply_eq_iff_eq, map_adj', Adj.ne]
} }
{ f with map_rel_iff' := by aesop (add simp map_adj') }

@[simp]
lemma map_apply (f : V ≃ W) (G : SimpleGraph V) (v : V) :
Expand Down
Loading