Lax Lean Archive

Atomically matched tuples

Lax185574.AtomicMatching · concepts/Lax185574/AtomicMatching.lean · lax-185574

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

    For a graph G and tuples ā, b̄ ∈ V(G)^t, the tuples ā = a₁ … a_t and b̄ = b₁ … b_t are atomically matched if there is a relation ∼ ∈ {=, ≠, ≥} such that G ⊨ E(aᵢ, bⱼ) if and only if i ∼ j, for all i, j ∈ [t]. In particular, the bipartite graph semi-induced between the tuples ā and b̄ is a matching, a co-matching, or a half-graph.

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

    In the paper

    • page 22 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2import Mathlib.Order.Fin.Basic
    3
    4/-!
    5---
    6title: Atomically matched tuples
    7type: definition
    8---
    9For a graph G and tuples ā, b̄ ∈ V(G)^t, the tuples ā = a₁ … a_t and
    10b̄ = b₁ … b_t are *atomically matched* if there is a relation
    11∼ ∈ {=, ≠, ≥} such that G ⊨ E(aᵢ, bⱼ) if and only if i ∼ j, for all
    12i, j ∈ [t]. In particular, the bipartite graph semi-induced between the
    13tuples ā and b̄ is a matching, a co-matching, or a half-graph.
    14
    15# Formalization notes
    16
    17Positions are `Fin t`, which is [t] shifted by one and carries the same
    18order. The relation i ≥ j is written j ≤ i. Only the adjacency between
    19the entries of ā and the entries of b̄ is constrained. The entries need
    20not be distinct, although the conditions force some distinctness, for
    21instance aᵢ ≠ bᵢ in the case of =.
    22-/
    23
    24namespace Lax185574.AtomicMatching
    25
    26universe u
    27
    28variable {V : Type u}
    29
    30/-- The tuples `a` and `b` are atomically matched in `G`: adjacency of
    31`a i` and `b j` is described by `i = j`, by `i ≠ j`, or by `i ≥ j`. -/
    32def AtomicallyMatched (G : SimpleGraph V) {t : ℕ} (a b : Fin t → V) : Prop :=
    33 (∀ i j, G.Adj (a i) (b j) ↔ i = j) ∨
    34 (∀ i j, G.Adj (a i) (b j) ↔ i ≠ j) ∨
    35 (∀ i j, G.Adj (a i) (b j) ↔ j ≤ i)
    36
    37end Lax185574.AtomicMatching
    38
    Formalization notes

    Positions are FintFin t, which is [t] shifted by one and carries the same order. The relation i ≥ j is written j ≤ i. Only the adjacency between the entries of ā and the entries of b̄ is constrained. The entries need not be distinct, although the conditions force some distinctness, for instance aᵢ ≠ bᵢ in the case of =.

    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…