Independent sets in hypergraphs

DefinitionIndependent set in a hypergraph#✓fully proved

Let \(H\) be a finite hypergraph, that is a finite family of finite sets of vertices, called its edges. A finite set \(I\) of vertices is independent in \(H\) when no edge \(e\) of \(H\) satisfies \(e \subseteq I\).

def IsIndependent (H : Finset (Finset V)) (I : Finset V) : Prop :=
  ∀ e ∈ H, ¬ e ⊆ I

Used by 4

Used byEvery set is independent in the empty hypergraph · When the empty set is independent · Independence unfolded · Subsets of independent sets are independent

TheoremIndependence unfolded#✓fully proved

A finite set \(I\) of vertices is independent in a finite hypergraph \(H\) if and only if no edge \(e\) of \(H\) satisfies \(e \subseteq I\).

theorem isIndependent_iff (H : Finset (Finset V)) (I : Finset V) :
    IsIndependent H I ↔ ∀ e ∈ H, ¬ e ⊆ I

Uses 1

Statement usesIndependent set in a hypergraph

TheoremEvery set is independent in the empty hypergraph#✓fully proved

Every finite set of vertices is independent in the empty hypergraph, the hypergraph with no edges.

theorem isIndependent_empty_hypergraph (I : Finset V) :
    IsIndependent (∅ : Finset (Finset V)) I

Uses 1

Statement usesIndependent set in a hypergraph

TheoremSubsets of independent sets are independent#✓fully proved

If a finite set \(I\) of vertices is independent in a finite hypergraph \(H\) and \(J \subseteq I\), then \(J\) is independent in \(H\).

theorem isIndependent_of_subset {H : Finset (Finset V)} {I J : Finset V}
    (h : IsIndependent H I) (hJI : J ⊆ I) : IsIndependent H J

Uses 1

Statement usesIndependent set in a hypergraph

TheoremWhen the empty set is independent#✓fully proved

For a finite hypergraph \(H\), the empty set is independent in \(H\) if and only if every edge of \(H\) is nonempty.

theorem isIndependent_empty_iff (H : Finset (Finset V)) :
    IsIndependent H ∅ ↔ ∀ e ∈ H, e.Nonempty

Uses 1

Statement usesIndependent set in a hypergraph

DefinitionSteiner triple system#✓fully proved

A finite hypergraph \(H\) on a vertex type \(V\), that is a finite family of finite subsets of \(V\), is a Steiner triple system when it is \(3\)-uniform (every edge of \(H\) has exactly \(3\) elements) and any two distinct vertices \(u \ne v\) of \(V\) lie together in exactly one edge of \(H\).

def IsSteinerTripleSystem (H : Finset (Finset V)) : Prop :=
  IsUniform H 3 ∧
    ∀ u v : V, u ≠ v → ∃! e : Finset V, e ∈ H ∧ u ∈ e ∧ v ∈ e

Uses 1 · Used by 3

Statement usesUniform hypergraphs

Used byErdős Problem 207 · Pairs in a Steiner triple system · Steiner triple systems are 3-uniform

TheoremSteiner triple systems are 3-uniform#✓fully proved

If \(H\) is a Steiner triple system, then \(H\) is \(3\)-uniform: every edge of \(H\) has exactly \(3\) elements.

theorem uniform_of_isSteinerTripleSystem {H : Finset (Finset V)}
    (h : IsSteinerTripleSystem H) : IsUniform H 3

Uses 2

Statement usesSteiner triple system · Uniform hypergraphs

TheoremPairs in a Steiner triple system#✓fully proved

If \(H\) is a Steiner triple system on a vertex type \(V\), then for all vertices \(u \ne v\) of \(V\) there is exactly one edge \(e\) of \(H\) with \(u \in e\) and \(v \in e\).

theorem pairCover_of_isSteinerTripleSystem {H : Finset (Finset V)}
    (h : IsSteinerTripleSystem H) :
    ∀ u v : V, u ≠ v → ∃! e : Finset V, e ∈ H ∧ u ∈ e ∧ v ∈ e

Uses 2

Statement usesSteiner triple system

Proof usesUniform hypergraphs

TheoremUnique element of a singleton family#✓fully proved

Let \(t\) be a finite set of vertices and let \(P\) be a property of finite sets of vertices. If \(t\) satisfies \(P\), then there is exactly one finite set \(e\) of vertices with \(e \in \{t\}\) and \(P(e)\).

theorem existsUnique_mem_singleton {t : Finset V} {P : Finset V → Prop}
    (hP : P t) : ∃! e : Finset V, e ∈ ({t} : Finset (Finset V)) ∧ P e

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.