InCover
plain-language theorem explainer
InCover is the predicate that a natural number vertex belongs to the list S of selected vertices. Researchers formalizing vertex cover instances in the Recognition Science complexity layer cite this predicate to build edge coverage checks. The definition is a direct one-line abbreviation to list membership.
Claim. Let $S$ be a list of natural numbers and $v$ a natural number. The proposition InCover$(S,v)$ holds if and only if $v$ is an element of $S$.
background
The Complexity.VertexCover module introduces predicates for the vertex cover problem inside the broader treatment of complexity pairs, which are functions of input size. InCover supplies the atomic membership test for whether a vertex lies inside a proposed cover set. The module imports Mathlib to access list operations and depends on the ILG action S from Relativity.ILG.Action.
proof idea
This is a one-line definition that unfolds directly to the standard list membership predicate ∈ on natural numbers.
why it matters
InCover is the building block for EdgeCovered, which asserts that an edge is covered when at least one endpoint satisfies the predicate. It supports the subsequent lemmas InCover_cons and InCover_of_mem that handle list cons and membership simplification. The definition therefore anchors the vertex cover machinery that sits inside the complexity domain of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.