is3Clique_iff_exists_cycle_length_three

English

Equivalent reformulations of 3-clique existence via a 3-length cycle, simplified.

Русский

Эквивалентные формулировки существования 3-клик через цикл длины 3, упрощённо.

LaTeX

$$$$ \\exists s:\\ Finset\\ α,\\ G.IsNClique 3 s \\iff \\exists u:\\ α, \\exists w:\\ G.Walk u u, w.IsCycle \\land w.length = 3 $$$$

Lean4

theorem is3Clique_iff_exists_cycle_length_three :
    (∃ s : Finset α, G.IsNClique 3 s) ↔ ∃ (u : α) (w : G.Walk u u), w.IsCycle ∧ w.length = 3 := by
  classical
  simp_rw [is3Clique_iff, isCycle_def]
  exact
    ⟨(fun ⟨_, a, _, _, hab, hac, hbc, _⟩ => ⟨a, cons hab (cons hbc (cons hac.symm nil)), by aesop⟩),
      (fun ⟨_, .cons hab (.cons hbc (.cons hca nil)), _, _⟩ => ⟨_, _, _, _, hab, hca.symm, hbc, rfl⟩)⟩

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