English
For a path p from a to b and a set S, if a ∉ S and b ∈ S, then p can be decomposed as p1 · e · p2 with e : u ⟶ v, p1 from a to u not in S, p2 from v to b with u ∉ S and v ∈ S.
Русский
Для пути p от a до b и множества S, если a ∉ S и b ∈ S, то путь можно разложить как p1 · e · p2, где e от u к v, p1 от a к u вне S, p2 от v к b, причём u ∉ S и v ∈ S.
LaTeX
$$∃ u ∉ S, ∃ v ∈ S, ∃ e: u ⟶ v, ∃ p1: Path a u, ∃ p2: Path v b, p = p1.comp (e.toPath.comp p2)$$
Lean4
/-- A path from a vertex not in `S` to a vertex in `S` must cross the boundary. -/
theorem exists_notMem_mem_hom_path_path_of_notMem_mem {a b : V} (p : Path a b) (S : Set V) (ha_not_in_S : a ∉ S)
(hb_in_S : b ∈ S) :
∃ᵉ (u ∉ S) (v ∈ S) (e : u ⟶ v) (p₁ : Path a u) (p₂ : Path v b), p = p₁.comp (e.toPath.comp p₂) := by
induction h_len : p.length generalizing a b S ha_not_in_S hb_in_S with
| zero =>
obtain rfl := eq_of_length_zero p h_len
exact (ha_not_in_S hb_in_S).elim
| succ n ih =>
have h_pos : 0 < p.length := by simp [h_len]
obtain ⟨c, p', e, rfl⟩ := (length_ne_zero_iff_eq_cons p).mp h_pos.ne'
by_cases hc_in_S : c ∈ S
· have p'_len : p'.length = n := by simp_all
obtain ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂, hp'⟩ := ih p' S ha_not_in_S hc_in_S p'_len
refine ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂.comp e.toPath, ?_⟩
simp [hp', comp_toPath_eq_cons]
· refine ⟨c, hc_in_S, b, hb_in_S, e, p', Path.nil, ?_⟩
simp [comp_toPath_eq_cons]
