Commit 2023-06-21 10:59 f52efae4

View on Github →

feat: port Archive.Wiedijk100Theorems.BallotProblem (#5204)

Estimated changes

Modified Archive.lean

Created Archive/Wiedijk100Theorems/BallotProblem.lean

added theorem Ballot.ballot_edge

added theorem Ballot.ballot_neg

added theorem Ballot.ballot_pos

added theorem Ballot.ballot_problem'

added theorem Ballot.ballot_problem

added theorem Ballot.ballot_same

added theorem Ballot.count_countedSequence

added def Ballot.countedSequence

added theorem Ballot.countedSequence_finite

added theorem Ballot.countedSequence_int_neg_counted_succ_succ

added theorem Ballot.countedSequence_int_pos_counted_succ_succ

added theorem Ballot.countedSequence_nonempty

added theorem Ballot.counted_eq_nil_iff

added theorem Ballot.counted_left_zero

added theorem Ballot.counted_ne_nil_left

added theorem Ballot.counted_ne_nil_right

added theorem Ballot.counted_right_zero

added theorem Ballot.counted_succ_succ

added theorem Ballot.disjoint_bits

added theorem Ballot.first_vote_neg

added theorem Ballot.first_vote_pos

added theorem Ballot.headI_mem_of_nonempty

added theorem Ballot.length_of_mem_countedSequence

added theorem Ballot.mem_countedSequence_iff_perm

added theorem Ballot.mem_of_mem_countedSequence

added def Ballot.staysPositive

added theorem Ballot.staysPositive_cons_pos

added theorem Ballot.staysPositive_nil

added theorem Ballot.sum_of_mem_countedSequence