Theorem SimpleGraph.Walk.notMem_support_takeUntil_support_takeUntil_subset

Modification history

2026-06-01 01:24

Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean

feat(Combinatorics/SimpleGraph/Walk): upgrade subset theorems to sublist/prefix/suffix (#37577) …

Modified SimpleGraph.Walk.notMem_support_takeUntil_support_takeUntil_subset View on Github →

2025-05-25 12:30

Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean

chore(*): not_mem/nmem -> notMem (#25159)

Added SimpleGraph.Walk.notMem_support_takeUntil_support_takeUntil_subset View on Github →