feat(SimpleGraph/Connectivity/Subgraph): w.toSubgraph.IsInduced ↔ w.IsChordless (#38568)

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

@@ -6,6 +6,7 @@ Authors: Kyle Miller, Rémi Bottinelli
 module
 
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
+public import Mathlib.Combinatorics.SimpleGraph.Walk.Chord
 public import Mathlib.Data.Set.Card
 
 /-!
@@ -366,6 +367,11 @@ theorem map_mapToSubgraph_eq_induce_id {u v : V} (w : G.Walk u v) :
       w.toSubgraph.coe →g G.induce _) = w.induce _ (fun _ ↦ id) :=
   w.map_mapToSubgraph_eq_induce ..
 
+theorem isInduced_toSubgraph {w : G.Walk u v} : w.toSubgraph.IsInduced ↔ w.IsChordless := by
+  simp_rw [Subgraph.IsInduced, IsChordless, IsChord, Sym2.forall, Sym2.lift_mk, G.mem_edgeSet,
+    mem_verts_toSubgraph, adj_toSubgraph_iff_mem_edges]
+  grind only
+
 namespace IsPath
 
 lemma neighborSet_toSubgraph_startpoint {u v} {p : G.Walk u v}