Theorem SimpleGraph.Walk.toSubgraph_le_iff

Modification history

2026-02-13 21:13

Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

feat(Combinatorics/SimpleGraph/Connectivity/Subgraph): `w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet` (#33527)

Added SimpleGraph.Walk.toSubgraph_le_iff View on Github →