Commit 2025-02-24 06:45 8c8ef3cd

View on Github →

feat(Combinatorics/SimpleGraph): takeUntil properties (#21250) Adds various results on takeUntil. In preparation for a proof of Tutte's theorem.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

added theorem SimpleGraph.Walk.mem_support_of_adj_toSubgraph

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean

added theorem SimpleGraph.Walk.getVert_takeUntil

added theorem SimpleGraph.Walk.length_takeUntil_lt

added theorem SimpleGraph.Walk.nil_takeUntil

added theorem SimpleGraph.Walk.not_mem_support_takeUntil_takeUntil

added theorem SimpleGraph.Walk.snd_takeUntil

added theorem SimpleGraph.Walk.takeUntil_cons

added theorem SimpleGraph.Walk.takeUntil_first

added theorem SimpleGraph.Walk.takeUntil_takeUntil

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.Walk.IsCycle.isPath_of_append_left

added theorem SimpleGraph.Walk.IsCycle.isPath_of_append_right

added theorem SimpleGraph.Walk.IsCycle.isPath_takeUntil

added theorem SimpleGraph.Walk.endpoint_not_mem_support_takeUntil

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.Nil.append

added theorem SimpleGraph.Walk.end_mem_tail_support

added theorem SimpleGraph.Walk.nil_append_iff

modified theorem SimpleGraph.Walk.nil_reverse