OAI/Combinatorics/BalancedRyser/Incidence/StabilityTangents.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.StabilityTangents.tangents line 13
  2. theorem OAI.Balanced.StabilityTangents.mem_tangents line 16
  3. theorem OAI.Balanced.StabilityTangents.intersection_card_zero_iff line 20
  4. theorem OAI.Balanced.StabilityTangents.sum_intersections_le_card line 24
  5. theorem OAI.Balanced.StabilityTangents.twice_card_le_intersections_and_small line 47
  6. theorem OAI.Balanced.StabilityTangents.sum_pencil_erase_filter_le line 71
  7. theorem OAI.Balanced.StabilityTangents.total_tangents_bound line 91
  8. theorem OAI.Balanced.StabilityTangents.sum_tangencies line 118
  9. theorem OAI.Balanced.StabilityTangents.exists_tangent_rich_point line 132
  10. theorem OAI.Balanced.StabilityTangents.skew_nonempty_of_card_le_order line 167
  11. theorem OAI.Balanced.StabilityTangents.card_skew_empty line 191
  12. theorem OAI.Balanced.StabilityTangents.nonempty_of_small_skew line 196
  13. theorem OAI.Balanced.StabilityTangents.exists_tangent_flag_with_margin line 205