Lax Lean Archive

Graph isomorphism relaxations

Lax871432.IsomorphismRelaxations · concepts/Lax871432/IsomorphismRelaxations.lean · lax-871432

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A graph isomorphism relaxation is an equivalence relation on finite simple graphs that is coarser than isomorphism: isomorphic graphs are related, and the relation is symmetric and transitive.

    Concept map
    1 concept; 12 descendants hidden
    100%
    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Maps
    2
    3/-!
    4---
    5title: Graph isomorphism relaxations
    6type: definition
    7---
    8A *graph isomorphism relaxation* is an equivalence relation on finite simple graphs that is
    9coarser than isomorphism: isomorphic graphs are related, and the relation is symmetric and
    10transitive.
    11-/
    12
    13namespace Lax871432.IsomorphismRelaxations
    14
    15/-- A *graph isomorphism relaxation*: an equivalence relation on finite simple graphs which
    16relates any two isomorphic graphs, and is therefore invariant under isomorphism. -/
    17structure GraphIsoRelaxation where
    18 /-- The relation itself. -/
    19 Rel : ∀ ⦃V W : Type⦄ [Finite V] [Finite W], SimpleGraph V → SimpleGraph W → Prop
    20 /-- Isomorphic graphs are related; in particular the relation is reflexive. -/
    21 rel_of_iso : ∀ {V W : Type} [Finite V] [Finite W] {G : SimpleGraph V} {H : SimpleGraph W},
    22 Nonempty (G ≃g H) → Rel G H
    23 /-- The relation is symmetric. -/
    24 symm : ∀ {V W : Type} [Finite V] [Finite W] {G : SimpleGraph V} {H : SimpleGraph W},
    25 Rel G H → Rel H G
    26 /-- The relation is transitive. -/
    27 trans : ∀ {U V W : Type} [Finite U] [Finite V] [Finite W] {G : SimpleGraph U}
    28 {H : SimpleGraph V} {K : SimpleGraph W}, Rel G H → Rel H K → Rel G K
    29
    30end Lax871432.IsomorphismRelaxations
    31
    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…