Lax Lean Archive

2-uniform set system

Lax683916.TwoUniformSetSystems · concepts/Lax683916/TwoUniformSetSystems.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 2-uniform set system on a ground type VV is a family of subsets of VV, each containing exactly two elements.

    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.Card
    2
    3/-!
    4---
    5title: 2-uniform set system
    6type: definition
    7---
    8A 2-uniform set system on a ground type `V` is a family of subsets of `V`,
    9each containing exactly two elements.
    10
    11# Formalization notes
    12
    13The family is represented as `Set (Set V)`, so it has neither repeated
    14members nor a separate ambient vertex set. No looplessness field is carried:
    15a singleton has cardinality one, so 2-uniformity already excludes loops.
    16-/
    17
    18namespace Lax683916.TwoUniformSetSystems
    19
    20/-- A family of two-element subsets of `V`. -/
    21structure TwoUniformSetSystem (V : Type*) where
    22 /-- The sets belonging to the family. -/
    23 sets : Set (Set V)
    24 /-- Every member of the family has exactly two elements. -/
    25 twoUniform : ∀ s ∈ sets, Set.ncard s = 2
    26
    27end Lax683916.TwoUniformSetSystems
    28
    Formalization notes

    The family is represented as Set(SetV)Set (Set V), so it has neither repeated members nor a separate ambient vertex set. No looplessness field is carried: a singleton has cardinality one, so 2-uniformity already excludes loops.

    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…