Finite hypergraphs: uniformity, partiteness, cover number, matching number, and Ryser's inequality

Preamble. The file imports only Mathlib's lattice structure on $\mathbb{N}$ (needed for the infimum/supremum of sets of natural numbers below). It declares one structure, FinHypergraph, and seven definitions in its namespace. After the structure, every definition is made in the context of a fixed type $V$ (in an arbitrary universe) that is assumed to carry a decidable equality (a typeclass assumption carried silently as an argument by each definition; it has no mathematical content, it is only what makes finite-set intersections well-defined) and a fixed finite hypergraph $H$ on $V$.

The structure FinHypergraph. For any type $\alpha$ (in any universe; no decidable-equality or other assumption on $\alpha$), a finite hypergraph $H$ on $\alpha$ consists of exactly three pieces of data: (i) a finite set $\mathrm{V}(H) \subseteq \alpha$, called the vertices; (ii) a set $\mathrm{E}(H)$ whose members are finite subsets of $\alpha$, called the edges — note that $\mathrm{E}(H)$ is an arbitrary set of finite subsets, not itself packaged as a finite set, although it is necessarily finite because of (iii); (iii) a proof that every edge is contained in the vertex set: for all $e \in \mathrm{E}(H)$, $e \subseteq \mathrm{V}(H)$. Nothing else is required: $\mathrm{V}(H)$ may be empty; $\mathrm{E}(H)$ may be empty; the empty set $\varnothing$ may be an edge; singletons may be edges; edges may have different sizes and may be nested in one another. Since $\mathrm{E}(H)$ is a set, there are no repeated edges.

$r$-uniform (IsUniform). For a natural number $r$ (including $r = 0$), $H$ is $r$-uniform iff every edge has exactly $r$ elements:

$$\forall e \in \mathrm{E}(H),\quad |e| = r .$$

Edge cases: if $\mathrm{E}(H) = \varnothing$, then $H$ is $r$-uniform for every $r$ simultaneously. $H$ is $0$-uniform iff every edge is the empty set, i.e. $\mathrm{E}(H) \subseteq \{\varnothing\}$.

$r$-partite (IsPartite). For a natural number $r$, $H$ is $r$-partite iff there exists a family of finite subsets $P_0, P_1, \dots, P_{r-1} \subseteq V$, indexed by $i \in \{0, 1, \dots, r-1\}$, such that all three of the following hold:

1. for every $v \in V$: $v \in \mathrm{V}(H)$ if and only if $v \in P_i$ for some index $i$ — equivalently $\bigcup_{i} P_i = \mathrm{V}(H)$;
2. for all indices $i \ne j$, $P_i \cap P_j = \varnothing$;
3. for every edge $e \in \mathrm{E}(H)$ and every index $i$, $|P_i \cap e| = 1$ (the edge meets each part in exactly one vertex).

Notes on what is not required: the parts are not required to be nonempty — if some $P_i = \varnothing$, condition 3 forces $\mathrm{E}(H) = \varnothing$, and the hypergraph is still $r$-partite. The family is not required to be unique. For $r = 0$ the index set is empty, so there is exactly one candidate family (the empty family); condition 1 then says that no $v$ lies in $\mathrm{V}(H)$, i.e. $\mathrm{V}(H) = \varnothing$, and conditions 2 and 3 hold vacuously; hence $H$ is $0$-partite iff it has no vertices. If $\mathrm{E}(H) = \varnothing$, condition 3 holds vacuously. If $\varnothing \in \mathrm{E}(H)$ and $r \ge 1$, condition 3 fails, so such an $H$ is not $r$-partite.

Vertex cover (IsVertexCover). A finite set $C \subseteq V$ is a vertex cover of $H$ iff $C \subseteq \mathrm{V}(H)$ and every edge contains some element of $C$:

$$C \subseteq \mathrm{V}(H) \quad\text{and}\quad \forall e \in \mathrm{E}(H),\ \exists v \in C,\ v \in e .$$

Edge cases: if $\mathrm{E}(H) = \varnothing$, then every subset of $\mathrm{V}(H)$, in particular $\varnothing$, is a vertex cover. If $\varnothing \in \mathrm{E}(H)$, no vertex cover exists at all. If no edge is empty, $\mathrm{V}(H)$ itself is a vertex cover.

Matching (IsMatching). A finite set $M$ of finite subsets of $V$ is a matching of $H$ iff every member of $M$ is an edge of $H$ and any two distinct members are disjoint:

$$M \subseteq \mathrm{E}(H) \quad\text{and}\quad \forall e_1, e_2 \in M,\ e_1 \ne e_2 \Rightarrow e_1 \cap e_2 = \varnothing .$$

Edge cases: $M = \varnothing$ is always a matching; any single edge $\{e\}$ with $e \in \mathrm{E}(H)$ is a matching; if $\varnothing \in \mathrm{E}(H)$, the empty edge may be a member of any matching, since it is disjoint from everything. Because $M$ is a set, an edge occurs in $M$ at most once.

Cover number (coverNumber). $\tau(H)$ is the natural number

$$\tau(H) \;=\; \inf\bigl\{\, n \in \mathbb{N} \;\bigm|\; \exists\, C \subseteq V \text{ finite},\ C \text{ is a vertex cover of } H \text{ and } |C| = n \,\bigr\},$$

where $\inf$ is Mathlib's infimum of a set of natural numbers: the least element of the set if the set is nonempty, and $0$ by convention if the set is empty. Hence: if at least one vertex cover exists, $\tau(H)$ is the minimum cardinality of a vertex cover; if no vertex cover exists (exactly when $\varnothing \in \mathrm{E}(H)$), $\tau(H) = 0$ as a junk value. Also $\tau(H) = 0$ when $\mathrm{E}(H) = \varnothing$ (the empty set is then a cover). So $\tau(H) = 0$ does not by itself distinguish "no edges" from "the empty edge is present".

Matching number (matchingNumber). $\nu(H)$ is the natural number

$$\nu(H) \;=\; \sup\bigl\{\, n \in \mathbb{N} \;\bigm|\; \exists\, M,\ M \text{ is a matching of } H \text{ and } |M| = n \,\bigr\},$$

where $\sup$ is Mathlib's supremum of a set of natural numbers: the least upper bound of the set if it is bounded above, and $0$ by convention if it is unbounded. The set here always contains $0$ (the empty matching) and is always bounded above, because every matching is a set of subsets of the finite set $\mathrm{V}(H)$, so $|M| \le 2^{|\mathrm{V}(H)|}$; consequently $\nu(H)$ is the maximum number of (distinct, pairwise disjoint) edges in a matching of $H$. In particular $\nu(H) = 0$ iff $\mathrm{E}(H) = \varnothing$, and if $\varnothing \in \mathrm{E}(H)$ the empty edge contributes at most $1$ to $|M|$.

Ryser's inequality for a fixed $r$ (RyserConjectureFor). For a natural number $r$, the proposition

$$\bigl(H \text{ is } r\text{-uniform}\bigr) \;\Longrightarrow\; \bigl(H \text{ is } r\text{-partite}\bigr) \;\Longrightarrow\; \tau(H) \;\le\; (r \mathbin{\dot-} 1)\cdot \nu(H),$$

where $r \mathbin{\dot-} 1$ is truncated natural-number subtraction: it equals $r - 1$ when $r \ge 1$ and $0$ when $r = 0$. The two hypotheses are premises of an implication (so the proposition is true whenever $H$ fails to be $r$-uniform or fails to be $r$-partite), the inequality is non-strict ($\le$), and the multiplication is in $\mathbb{N}$. For $r = 0$ and for $r = 1$ the right-hand side is $0$, so in those cases the conclusion is $\tau(H) = 0$. No lower bound on $r$ and no nonemptiness of $\mathrm{V}(H)$ or $\mathrm{E}(H)$ is imposed in this definition.