Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Graphs sampled from a hole relation

Lax342547.SampledGraph · concepts/Lax342547/SampledGraph.lean · lax-342547

proven

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

    Lemma

    Given a symmetric relation of holes and a list of raw vertices, join two distinct positions exactly when their entries have no hole. Repeated raw vertices are permitted. If the hole relation has no triangles, every independent set of the sampled graph has size at most two, as in (2.2).

    Concept map
    1 concept
    100%
    Proven claimThis conceptDescendants are omitted for concepts with more than 10 descendants.
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Clique
    2
    3/-!
    4---
    5title: Graphs sampled from a hole relation
    6type: lemma
    7---
    8Given a symmetric relation of holes and a list of raw vertices, join two
    9distinct positions exactly when their entries have no hole. Repeated raw
    10vertices are permitted. If the hole relation has no triangles, every
    11independent set of the sampled graph has size at most two, as in (2.2).
    12-/
    13
    14namespace Lax342547.SampledGraph
    15
    16universe u
    17
    18def sampleGraph {Ω : Type u} (hole : Ω → Ω → Prop) (hsymm : (∀ ⦃i j⦄, hole i j → hole j i))
    19 {m : ℕ} (sample : Fin m → Ω) : SimpleGraph (Fin m) where
    20 Adj i j := i ≠ j ∧ ¬ hole (sample i) (sample j)
    21 symm := ⟨fun _ _ h ↦ ⟨h.1.symm, fun h' ↦ h.2 (hsymm h')⟩⟩
    22 loopless := ⟨fun _ h ↦ h.1 rfl⟩
    23
    24axiom sampleGraph_indepNum_le_two {Ω : Type u}
    25 (hole : Ω → Ω → Prop) (hsymm : (∀ ⦃i j⦄, hole i j → hole j i))
    26 (htriangle : ∀ i j k, hole i j → hole j k → ¬ hole k i)
    27 {m : ℕ} (sample : Fin m → Ω) :
    28 (sampleGraph hole hsymm sample).indepNum ≤ 2
    29
    30end Lax342547.SampledGraph
    31
    Show Proof
    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…