Formal target: Corpus.Reconstruction.conjecture

For finite simple graphs G on V and H on W (Mathlib SimpleGraph, Fintype vertices) with at least three vertices, if there is a bijection σ : V ≃ W with G.induce {v}ᶜ isomorphic (≃g) to H.induce {σ v}ᶜ for every v, then G ≃g H is nonempty; the bijection encodes equality of the multisets of card isomorphism classes.

Exact formal statement

∀ {V W : Type} [inst : Fintype.{0} V] [Fintype.{0} W] (G : SimpleGraph.{0} V) (H : SimpleGraph.{0} W),
  LE.le.{0} 3 (Fintype.card.{0} V) →
    (Exists.{1} fun σ =>
        ∀ (v : V),
          Nonempty.{1}
            (SimpleGraph.Iso.{0, 0} (SimpleGraph.induce.{0} (Compl.compl.{0} (Singleton.singleton.{0, 0} v)) G)
              (SimpleGraph.induce.{0} (Compl.compl.{0} (Singleton.singleton.{0, 0} (DFunLike.coe.{1, 1, 1} σ v))) H))) →
      Nonempty.{1} (SimpleGraph.Iso.{0, 0} G H)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record