edgeDisjointTriangles_iff_mem_sym2_subsingleton

English

A graph has edge-disjoint triangles if and only if for every non-diagonal Sym2-edge e, the collection of 3-cliques containing e forms a Subsingleton set.

Русский

Граф имеет непересекающиеся треугольники тогда и только тогда, когда для каждого ребра e в Sym2 α, не диагонального типа, множество 3- clique, содержащих e, образует подмножество-одиночность.

LaTeX

$$$G.\\text{EdgeDisjointTriangles} \\iff \\forall\\{e:\\mathrm{Sym2}\\,\\alpha\\}, \\neg e.\\text{IsDiag} \\to \\{s\\in G.cliqueSet 3 \\mid e\\in s.\\sym2\\}.\\text{Subsingleton}$$$

Lean4

theorem edgeDisjointTriangles_iff_mem_sym2_subsingleton :
    G.EdgeDisjointTriangles ↔ ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s ∈ G.cliqueSet 3 | e ∈ (s : Finset α).sym2}.Subsingleton :=
  by
  classical
  have (a b) (hab : a ≠ b) :
    {s ∈ (G.cliqueSet 3 : Set (Finset α)) | s(a, b) ∈ (s : Finset α).sym2} =
      {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = { a, b, c }} :=
    by
    ext s
    simp only [mem_sym2_iff, Sym2.mem_iff, forall_eq_or_imp, forall_eq, mem_cliqueSet_iff, Set.mem_setOf_eq,
      is3Clique_iff]
    constructor
    · rintro ⟨⟨c, d, e, hcd, hce, hde, rfl⟩, hab⟩
      simp only [mem_insert, mem_singleton] at hab
      obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
      any_goals simp only [*, adj_comm, true_and, Ne, not_true] at *
      any_goals
        first
        | exact ⟨c, by aesop⟩
        | exact ⟨d, by aesop⟩
        | exact ⟨e, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨c, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨d, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨e, by aesop⟩
    · rintro ⟨hab, c, hac, hbc, rfl⟩
      refine ⟨⟨a, b, c, ?_⟩, ?_⟩ <;> simp [*]
  constructor
  · rw [Sym2.forall]
    rintro hG a b hab
    simp only [Sym2.isDiag_iff_proj_eq] at hab
    rw [this _ _ (Sym2.mk_isDiag_iff.not.2 hab)]
    rintro _ ⟨hab, c, hac, hbc, rfl⟩ _ ⟨-, d, had, hbd, rfl⟩
    refine hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩) <;> simp [is3Clique_triple_iff, *]
  · simp only [EdgeDisjointTriangles, is3Clique_iff, Set.Pairwise, mem_cliqueSet_iff, Ne, forall_exists_index, and_imp,
      ← Set.not_nontrivial_iff (s := _ ∩ _), not_imp_not, Set.Nontrivial, Set.mem_inter_iff, mem_coe]
    rintro hG _ a b c hab hac hbc rfl _ d e f hde hdf hef rfl g hg₁ hg₂ h hh₁ hh₂ hgh
    refine
        hG (Sym2.mk_isDiag_iff.not.2 hgh) ⟨⟨a, b, c, ?_⟩, by simpa using And.intro hg₁ hh₁⟩
          ⟨⟨d, e, f, ?_⟩, by simpa using And.intro hg₂ hh₂⟩ <;>
      simp [*]

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