exists_ne_odd_degree_of_exists_odd_degree

English

If there exists a vertex with odd degree, there exists another vertex with odd degree.

Русский

Если существует вершина нечетной степени, существует другая вершина нечетной степени.

LaTeX

$$∃ v (Odd(G.degree v)) ⇒ ∃ w ≠ v (Odd(G.degree w))$$

Lean4

theorem exists_ne_odd_degree_of_exists_odd_degree [Fintype V] [DecidableRel G.Adj] (v : V) (h : Odd (G.degree v)) :
    ∃ w : V, w ≠ v ∧ Odd (G.degree w) := by
  haveI := Classical.decEq V
  rcases G.odd_card_odd_degree_vertices_ne v h with ⟨k, hg⟩
  have hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)} := by
    rw [hg]
    apply Nat.succ_pos
  rcases card_pos.mp hg' with ⟨w, hw⟩
  rw [mem_filter_univ] at hw
  exact ⟨w, hw⟩

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