isClique_iff_induce_eq — Mathlib

English

G.IsClique s is equivalent to the induced subgraph on s being the complete graph.

Русский

Утверждение G.IsClique s эквивалентно тому, что индуцированный на s граф является полным графом.

LaTeX

$$$ G.IsClique s \iff G.induce s = \top $$$

Lean4

/-- A clique is a set of vertices whose induced graph is complete. -/
theorem isClique_iff_induce_eq : G.IsClique s ↔ G.induce s = ⊤ :=
  by
  rw [isClique_iff]
  constructor
  · intro h
    ext ⟨v, hv⟩ ⟨w, hw⟩
    simp only [comap_adj, top_adj, Ne, Subtype.mk_eq_mk]
    exact ⟨Adj.ne, h hv hw⟩
  · intro h v hv w hw hne
    have h2 : (G.induce s).Adj ⟨v, hv⟩ ⟨w, hw⟩ = _ := rfl
    conv_lhs at h2 => rw [h]
    simp only [top_adj, ne_eq, Subtype.mk.injEq, eq_iff_iff] at h2
    exact h2.1 hne

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