is3Clique_iff — Mathlib

English

Exists a 3-clique exactly when there exists a cycle of length 3 in the graph.

Русский

Существует 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 : G.IsNClique 3 s ↔ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = { a, b, c } :=
  by
  refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨a, b, c, -, -, -, hs⟩ := card_eq_three.1 h.card_eq
    refine ⟨a, b, c, ?_⟩
    rwa [hs, eq_self_iff_true, and_true, is3Clique_triple_iff.symm, ← hs]
  · rintro ⟨a, b, c, hab, hbc, hca, rfl⟩
    exact is3Clique_triple_iff.2 ⟨hab, hbc, hca⟩

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