English
Given a set S and a walk p from u to v with u ∈ S and v ∉ S, there exists a dart in p.darts whose start is in S and end is not in S.
Русский
Для множества S и хода p от u до v с u ∈ S и v ∉ S существует дарт в p.darts, начинающийся в S и оканчивающийся вне S.
LaTeX
$$$ \\exists d: G.Dart, d \\in p.darts \\land d.fst \\in S \\land d.snd \\notin S $$$
Lean4
/-- Given a set `S` and a walk `w` from `u` to `v` such that `u ∈ S` but `v ∉ S`,
there exists a dart in the walk whose start is in `S` but whose end is not. -/
theorem exists_boundary_dart {u v : V} (p : G.Walk u v) (S : Set V) (uS : u ∈ S) (vS : v ∉ S) :
∃ d : G.Dart, d ∈ p.darts ∧ d.fst ∈ S ∧ d.snd ∉ S := by
induction p with
| nil => cases vS uS
| cons a p' ih =>
rename_i x y w
by_cases h : y ∈ S
· obtain ⟨d, hd, hcd⟩ := ih h vS
exact ⟨d, List.Mem.tail _ hd, hcd⟩
· exact ⟨⟨(x, y), a⟩, List.Mem.head _, uS, h⟩
