pathGraph_le_cycleGraph — Mathlib

English

For every n, the path graph on n vertices is a subgraph of the cycle graph on n vertices.

Русский

Для любого n граф пути на n вершинах является подграфом графа цикла на n вершинах.

LaTeX

$$$ pathGraph\ n \le\ cycleGraph\ n $$$

Lean4

theorem pathGraph_le_cycleGraph {n : ℕ} : pathGraph n ≤ cycleGraph n := by
  match n with
  | 0 | 1 => simp
  | n + 2 =>
    intro u v h
    rw [pathGraph_adj] at h
    rw [cycleGraph_adj']
    cases h with
    | inl h
    | inr h => simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]

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