OAI/Combinatorics/Ryser/Hypergraph/Partite.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.RyserCoveringCounterexample.PartiteUniform.edgePart_bijectiveline 11 - theorem
OAI.RyserCoveringCounterexample.PartiteUniform.edge_cardline 23 - theorem
OAI.RyserCoveringCounterexample.PartiteUniform.uniformline 29 - theorem
OAI.RyserCoveringCounterexample.RPartiteUniform.uniformline 34 - theorem
OAI.RyserCoveringCounterexample.Uniform.nonemptyEdgesline 40 - theorem
OAI.RyserCoveringCounterexample.RPartiteUniform.nonemptyEdgesline 47 - theorem
OAI.RyserCoveringCounterexample.PartiteUniform.relabelline 51 - theorem
OAI.RyserCoveringCounterexample.PartiteUniform.rPartiteUniformline 64