Uniform hypergraphs

DefinitionUniform hypergraphs#✓fully proved

Let \(H\) be a finite family of finite subsets of a type \(V\), viewed as a hypergraph with edge set \(H\), and let \(r \in \mathbb{N}\). Then \(H\) is \(r\)-uniform when every edge \(e \in H\) has exactly \(r\) elements.

public def IsUniform {V : Type*} (H : Finset (Finset V)) (r : ℕ) : Prop :=
  ∀ e ∈ H, e.card = r

Used by 17

Used bySteiner triple system · Pairs in a Steiner triple system · Steiner triple systems are 3-uniform · Erdős Problem 834 for transversal-critical triple systems · Erdős Problem 794 on dense 3-uniform hypergraphs · Extremal number for \(k\) vertices spanning \(k - 2\) triples · Turán number of the generalized triangle · Steiner system \(S(t, r, m)\) · The complete \(r\)-graph is a Turán system · The complete \(r\)-graph is \(r\)-uniform · Turán systems cover every \(s\)-set · Turán system · A Turán system has \(s \le n\) · A Turán system has \(r < s\) · Turán systems have positive uniformity · Turán systems are uniform · Characterization of uniform hypergraphs

DefinitionSubhypergraph containment#✓fully proved

Let \(H\) be a finite family of finite subsets of a type \(V\), viewed as a hypergraph with edge set \(H\), and let \(m, k \in \mathbb{N}\). Then \(H\) contains a subgraph with \(m\) vertices and at least \(k\) edges when there is a set \(S\) of exactly \(m\) elements of \(V\) such that at least \(k\) edges of \(H\) are subsets of \(S\).

public def ContainsSubgraph {V : Type*} [DecidableEq V]
    (H : Finset (Finset V)) (m k : ℕ) : Prop :=
  ∃ S : Finset V, S.card = m ∧
    k ≤ (H.filter fun e => e ⊆ S).card

Used by 3

Used byErdős Problem 794 on dense 3-uniform hypergraphs · Extremal number for \(k\) vertices spanning \(k - 2\) triples · Characterization of subhypergraph containment

TheoremCharacterization of uniform hypergraphs#✓fully proved

Let \(H\) be a finite family of finite subsets of a type \(V\) and let \(r \in \mathbb{N}\). Then \(H\) is \(r\)-uniform if and only if every member \(e \in H\) has exactly \(r\) elements.

public theorem isUniform_iff {V : Type*} (H : Finset (Finset V)) (r : ℕ) :
    IsUniform H r ↔ ∀ e ∈ H, e.card = r

Uses 1

Statement usesUniform hypergraphs

TheoremCharacterization of subhypergraph containment#✓fully proved

Let \(H\) be a finite family of finite subsets of a type \(V\) and let \(m, k \in \mathbb{N}\). Then \(H\) contains a subgraph with \(m\) vertices and at least \(k\) edges if and only if there is a set \(S\) of exactly \(m\) elements of \(V\) such that at least \(k\) members of \(H\) are subsets of \(S\).

public theorem containsSubgraph_iff {V : Type*} [DecidableEq V]
    (H : Finset (Finset V)) (m k : ℕ) :
    ContainsSubgraph H m k ↔
      ∃ S : Finset V, S.card = m ∧ k ≤ (H.filter fun e => e ⊆ S).card

Uses 1

Statement usesSubhypergraph containment

DefinitionIntersecting families#✓fully proved

Let \(F\) be a finite family of finite subsets of a type \(\alpha\). Then \(F\) is intersecting when every two distinct members meet: for all \(A, B \in F\) with \(A \neq B\), the intersection \(A \cap B\) is nonempty.

The distinctness is load-bearing: the singleton family \(\{\emptyset\}\) is intersecting.

public def IsIntersecting {α : Type*} [DecidableEq α] (F : Finset (Finset α)) :
    Prop :=
  ∀ A ∈ F, ∀ B ∈ F, A ≠ B → (A ∩ B).Nonempty

Used by 2

Used byChvátal's conjecture · Characterization of intersecting families

TheoremCharacterization of intersecting families#✓fully proved

Let \(F\) be a finite family of finite subsets of a type \(\alpha\). Then \(F\) is intersecting if and only if for all \(A, B \in F\) with \(A \neq B\), the intersection \(A \cap B\) is nonempty.

public theorem isIntersecting_iff {α : Type*} [DecidableEq α]
    (F : Finset (Finset α)) :
    IsIntersecting F ↔ ∀ A ∈ F, ∀ B ∈ F, A ≠ B → (A ∩ B).Nonempty

Uses 1

Statement usesIntersecting families

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.