OAI/Combinatorics/BalancedRyser/Candidates/CandidateConstituentTail.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.CandidateConstituentTail.power_tail_le line 16
  2. theorem OAI.Balanced.CandidateConstituentTail.constituent_codes_eq line 35
  3. theorem OAI.Balanced.CandidateConstituentTail.mem_constituent_codes_iff line 39
  4. theorem OAI.Balanced.CandidateConstituentTail.exposedLaw_empty line 44
  5. theorem OAI.Balanced.CandidateConstituentTail.conditional_constituent_tail_le line 51
  6. def OAI.Balanced.CandidateConstituentTail.tailConstant line 71
  7. theorem OAI.Balanced.CandidateConstituentTail.single_direction_tail_le line 73
  8. theorem OAI.Balanced.CandidateConstituentTail.some_direction_tail_le line 89
  9. theorem OAI.Balanced.CandidateConstituentTail.tendsto_some_direction_tail line 124