English
For any finite set s of vertices, if there is a vertex in s that lies in the walk’s support, there exists a vertex x in s such that after erasing x and taking until x, the remaining support is empty.
Русский
Для любого конечного множества вершин s, если есть вершина из s, принадлежащая поддержке обхода, существует x ∈ s такое, что после удаления x и применения takeUntil оставшаяся поддержка пустая.
LaTeX
$$$ (s : Finset V) \, (h : {x \in s | x \in p.support}.Nonempty) \Rightarrow \exists x \in s, \exists hx : x \in p.support, {t \in s.erase x | t \in (p.takeUntil x hx).support} = \emptyset $$$
Lean4
/-- This lemma states that given some finite set of vertices, of which at least one is in the
support of a given walk, one of them is the first to be encountered. This consequence is encoded
as the set of vertices, restricted to those in the support, except for the first, being empty.
You could interpret this as being `takeUntilSet`, but defining this is slightly involved due to
not knowing what the final vertex is. This could be done by defining a function to obtain the
first encountered vertex and then use that to define `takeUntilSet`. That direction could be
worthwhile if this concept is used more widely. -/
theorem exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty (s : Finset V)
(h : {x ∈ s | x ∈ p.support}.Nonempty) :
∃ x ∈ s, ∃ hx : x ∈ p.support, {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅ :=
by
simp only [← Finset.subset_empty]
induction hp : p.length + #s using Nat.strong_induction_on generalizing s v with
| _ n ih
simp only [Finset.Nonempty, mem_filter] at h
obtain ⟨x, hxs, hx⟩ := h
obtain h | h := Finset.eq_empty_or_nonempty ({t ∈ s.erase x | t ∈ (p.takeUntil x hx).support})
· use x, hxs, hx, h.le
have : (p.takeUntil x hx).length + #(s.erase x) < n :=
by
rw [← card_erase_add_one hxs] at hp
have := p.length_takeUntil_le hx
omega
obtain ⟨y, hys, hyp, h⟩ := ih _ this (s.erase x) h rfl
use y, mem_of_mem_erase hys, support_takeUntil_subset p hx hyp
rwa [takeUntil_takeUntil, erase_right_comm, filter_erase, erase_eq_of_notMem] at h
simp only [mem_filter, mem_erase, ne_eq, not_and, and_imp]
rintro hxy -
exact notMem_support_takeUntil_support_takeUntil_subset (Ne.symm hxy) hx hyp
