OAI/Combinatorics/SharpRamsey/Construction/FlagConstruction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpLogRamsey.flag_vectors_independent line 12
  2. theorem OAI.SharpLogRamsey.flag_length_lt_finrank line 38
  3. theorem OAI.SharpLogRamsey.incident_iff_submodule line 59
  4. def OAI.SharpLogRamsey.flagGraph line 65
  5. theorem OAI.SharpLogRamsey.flagGraph_adj_of_lt line 76
  6. theorem OAI.SharpLogRamsey.flagGraph_cliqueFree line 83
  7. theorem OAI.SharpLogRamsey.consistent_iff_no_edges line 108
  8. def OAI.SharpLogRamsey.ConsistentOn line 119
  9. theorem OAI.SharpLogRamsey.consistentOn_iff_compl_isClique line 123
  10. def OAI.SharpLogRamsey.projectiveSubmoduleEquiv line 138
  11. theorem OAI.SharpLogRamsey.card_incident_points line 162
  12. theorem OAI.SharpLogRamsey.card_flags line 175
  13. theorem OAI.SharpLogRamsey.prime_flagGraph_cliqueFree line 206