Skip to content

Commit

Permalink
remove duplicate lemma
Browse files Browse the repository at this point in the history
  • Loading branch information
Christoph Spiegel committed Oct 28, 2024
1 parent 663639b commit 56b2d87
Showing 1 changed file with 0 additions and 7 deletions.
7 changes: 0 additions & 7 deletions Mathlib/Combinatorics/SimpleGraph/IndependentSet.lean
Original file line number Diff line number Diff line change
Expand Up @@ -91,13 +91,6 @@ protected theorem IsIndependentSet.map (h : G.IsIndependentSet s) {f : α ↪ β
have haneb : a ≠ b := fun a' ↦ hab (congrArg (⇑f) a')
simp [h ha hb haneb]

@[simp] -- TODO this should live in Clique.lean also the aesop is expensve...
lemma isClique_compl_map_iff_isClique_map_compl {f : α ↪ β} {s : Set α} :
(SimpleGraph.map f G)ᶜ.IsClique (f '' s) ↔ (SimpleGraph.map f Gᶜ).IsClique (f '' s) := by
repeat rw [isClique_iff];
repeat rw [Set.Pairwise];
aesop

@[simp] theorem isIndependentSet_map_image_iff {f : α ↪ β} :
(G.map f).IsIndependentSet (f '' s) ↔ G.IsIndependentSet s := by
constructor
Expand Down

0 comments on commit 56b2d87

Please sign in to comment.