Lax Lean Archive

Lax5.MonadicDependence

Monadic dependence

concepts/Lax5/MonadicDependence.lean · lax-5

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    A graph class is monadically dependent (also called monadically NIP) if it does not transduce the class of all graphs.

    Lean source view on GitHub

    1import Lax5.GraphClasses
    2import Lax5.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 Lax5.MonadicDependence
    20
    21open Lax12.GraphClasses Lax5.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 Lax5.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

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…