Lax Lean Archive

Neighborhood set system

Lax683916.NeighborhoodSetSystems · concepts/Lax683916/NeighborhoodSetSystems.lean · lax-683916

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 neighborhood set system on VV assigns a subset of VV to every vertex. Membership is symmetric, and no vertex belongs to its own neighborhood.

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

    Lean source view on GitHub

    1import Mathlib.Data.Set.Basic
    2
    3/-!
    4---
    5title: Neighborhood set system
    6type: definition
    7---
    8A neighborhood set system on `V` assigns a subset of `V` to every vertex.
    9Membership is symmetric, and no vertex belongs to its own neighborhood.
    10
    11# Formalization notes
    12
    13The family is indexed by `V`, rather than represented only by its range as a
    14`Set (Set V)`. Keeping the index records which vertex owns each neighborhood
    15and permits distinct vertices to have equal neighborhoods. The two laws are
    16exactly symmetry and irreflexivity of the associated membership relation.
    17-/
    18
    19namespace Lax683916.NeighborhoodSetSystems
    20
    21universe u
    22
    23/-- A vertex-indexed family of open neighborhoods. -/
    24structure NeighborhoodSetSystem (V : Type u) where
    25 /-- The open neighborhood assigned to each vertex. -/
    26 neighborhood : V → Set V
    27 /-- Neighborhood membership is symmetric. -/
    28 symmetric : ∀ u v : V, v ∈ neighborhood u ↔ u ∈ neighborhood v
    29 /-- A vertex does not belong to its own open neighborhood. -/
    30 loopless : ∀ u : V, u ∉ neighborhood u
    31
    32end Lax683916.NeighborhoodSetSystems
    33
    Formalization notes

    The family is indexed by VV, rather than represented only by its range as a Set(SetV)Set (Set V). Keeping the index records which vertex owns each neighborhood and permits distinct vertices to have equal neighborhoods. The two laws are exactly symmetry and irreflexivity of the associated membership relation.

    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…