is3Clique_triple_iff — Mathlib

English

There exists a 3-clique if and only if 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:\\, w.IsCycle \\land w.length = 3 $$$$

Lean4

theorem is3Clique_triple_iff : G.IsNClique 3 { a, b, c } ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c :=
  by
  simp only [isNClique_iff, Set.pairwise_insert_of_symmetric G.symm, coe_insert]
  by_cases hab : a = b <;> by_cases hbc : b = c <;> by_cases hac : a = c <;> subst_vars <;> simp [and_rotate, *]

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