OAI/Combinatorics/BalancedRyser/Candidates/CandidateExposedWitness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.CandidateExposedWitness.forcedPoint line 11
2. theorem OAI.Balanced.CandidateExposedWitness.forcedPoint_on_target line 14
3. theorem OAI.Balanced.CandidateExposedWitness.forcedPoint_on_constituent line 18
4. theorem OAI.Balanced.CandidateExposedWitness.eq_forcedPoint line 23
5. theorem OAI.Balanced.CandidateExposedWitness.pairWitness_iff_forcedPoints line 32
6. theorem OAI.Balanced.CandidateExposedWitness.successful_opposite_iff_fixed_positions line 50
7. theorem OAI.Balanced.CandidateExposedWitness.exists_external_iff_forcedPoint line 59
8. theorem OAI.Balanced.CandidateExposedWitness.external_point_unique line 73