Lax Lean Archive

Monadic dependence

Lax710763.MonadicDependence · concepts/Lax710763/MonadicDependence.lean · lax-710763

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 class is monadically dependent (also called monadically NIP) if it does not transduce the class of all graphs.

    Concept map
    5 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax710763.GraphClasses
    2import Lax710763.GraphTransductions
    3
    4/-!
    5---
    6title: Monadic dependence
    7type: definition
    8---
    9A graph class is monadically dependent (also called monadically NIP) if
    10it does not transduce the class of all graphs.
    11
    12# Formalization notes
    13
    14This is the standard transduction-based definition from the model theory
    15of graph classes, stated over the transduction relation of the
    16prerequisite concepts.
    17-/
    18
    19namespace Lax710763.MonadicDependence
    20
    21open Lax199508.GraphClasses Lax710763.GraphClasses
    22
    23/-- A graph class is monadically dependent if it does not transduce the
    24class of all finite simple graphs. -/
    25def MonadicallyDependent (C : GraphClass) : Prop :=
    26 ¬ GraphTransductions.Transduces C allGraphs
    27
    28end Lax710763.MonadicDependence
    29
    Formalization notes

    This is the standard transduction-based definition from the model theory of graph classes, stated over the transduction relation of the prerequisite concepts.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…