LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Hall's condition passes to the strict and tight induction subinstances

Statement

Let $(X, Y)$ satisfy Hall's condition. If $∣ X ∣ \geq 2$ , then exactly one of the following usable reductions holds.

Strict case: if $∣ N (S) ∣ > ∣ S ∣$ for every nonempty proper $S \subset X$ , then for every edge $x y$ the graph obtained by deleting $x$ and $y$ satisfies Hall's condition on $X ∖ {x}$ .
Tight case: if some nonempty proper $S \subset X$ has $∣ N (S) ∣ = ∣ S ∣$ , then both the subgraph on $S \cup N (S)$ and the subgraph on $(X ∖ S) \cup (Y ∖ N (S))$ satisfy Hall's condition on their respective left parts.

Facts & Assumptions

Given: A finite bipartite graph with parts $(X, Y)$ satisfying Hall's condition.

[F1]

Hall's condition says $∣ N (T) ∣ \geq ∣ T ∣$ for every left subset $T \subseteq X$ (Bipartite neighbourhoods, Hall's condition and systems of distinct representatives).

Proof

technique · direct

1.1

In the strict case, let $x y$ be an edge and $T \subseteq X ∖ {x}$ ; if $T$ is nonempty then $T$ is proper in $X$ , so $∣ N (T) ∣ > ∣ T ∣$ and deleting $y$ leaves at least $∣ T ∣$ neighbours.

1.2

Thus the graph with $x, y$ deleted satisfies Hall's condition on $X ∖ {x}$ , including $T = \emptyset$ .

2.1

In the tight case, $T \subseteq S$ has $∣ N (T) \cap N (S) ∣ = ∣ N (T) ∣ \geq ∣ T ∣$ , while $T \subseteq X ∖ S$ with fewer than $∣ T ∣$ neighbours outside $N (S)$ would make $∣ N (T \cup S) ∣ < ∣ T \cup S ∣$ ; both induced subinstances therefore satisfy Hall.

step 1.2

3.1

Steps 1.1--2.1 establish the strict and tight reductions.

step 1.2step 2.1∎

Remarks

The two alternatives are exhaustive by whether a nonempty proper left subset is tight; the one-vertex case is kept in Hall's theorem rather than forced into this reduction.

Depends on

Used by

Hall's marriage theorem for a finite bipartite graph Theorem

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

F. Gotti, Matching and Hall's Theorem (standard reference, not scraped)