OAI/Combinatorics/BalancedRyser/Incidence/AffineDirectionCounting.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.direction_eq_of_common_point line 11
  2. theorem OAI.Balanced.existsUnique_direction_of_ne line 20
  3. theorem OAI.Balanced.card_directions_to_point line 35
  4. theorem OAI.Balanced.card_directions_meeting_pair_away_le_one line 46
  5. theorem OAI.Balanced.card_projection_directions_le_one line 59
  6. theorem OAI.Balanced.projection_direction_fraction_le line 74
  7. theorem OAI.Balanced.projection_uniform_probability_le line 84
  8. theorem OAI.Balanced.point_uniform_direction_probability line 96