exists_mem_notMem_hom_path_path_of_notMem_mem

English

If a path p from a to b and S satisfies a ∈ S and b ∉ S, then p can be decomposed with a start in S and end outside, analogously to the previous lemma.

Русский

Если путь p от a до b и a ∈ S, b ∉ S, то путь можно разложить аналогично предыдущему лемме с началом в S и концом вне S.

LaTeX

$$exists_mem_notMem_hom_path_path_of_notMem_mem$$

Lean4

theorem exists_mem_notMem_hom_path_path_of_notMem_mem {a b : V} (p : Path a b) (S : Set V) (ha_in_S : a ∈ S)
    (hb_not_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
  classical
  have ha_not_in_compl : a ∉ Sᶜ := by simpa
  have hb_in_compl : b ∈ Sᶜ := by simpa
  obtain ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩ :=
    exists_notMem_mem_hom_path_path_of_notMem_mem p Sᶜ ha_not_in_compl hb_in_compl
  simp only [Set.mem_compl_iff, not_not] at hu_not_in_compl hv_in_compl
  refine ⟨u, hu_not_in_compl, v, hv_in_compl, e, p₁, p₂, hp⟩

Похожие утверждения