OAI/ModelTheory/Choiceless/Bounds.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CPTSeparation.Grid.four_fibers line 13
  2. theorem OAI.CPTSeparation.Grid.edgeFaces_card_le line 38
  3. def OAI.CPTSeparation.Grid.localSizeBound line 86
  4. theorem OAI.CPTSeparation.Grid.localGroup_card_le line 88
  5. theorem OAI.CPTSeparation.Grid.configuration_card_le line 99
  6. def OAI.CPTSeparation.Grid.atomSizeConstant line 111
  7. theorem OAI.CPTSeparation.Grid.atom_card_bounds line 113
  8. theorem OAI.CPTSeparation.Hereditary.hereditary_iff line 148
  9. theorem OAI.CPTSeparation.Hereditary.hereditary_transitive line 158
  10. theorem OAI.CPTSeparation.Hereditary.ordinal_hereditary line 161
  11. abbrev OAI.CPTSeparation.Grid.programInput line 184
  12. def OAI.CPTSeparation.Grid.programActionIso line 189
  13. theorem OAI.CPTSeparation.Grid.trace_supported line 195
  14. def OAI.CPTSeparation.Grid.programDomain line 211
  15. def OAI.CPTSeparation.Grid.programHF line 213
  16. theorem OAI.CPTSeparation.Grid.program_domain_transitive line 216
  17. theorem OAI.CPTSeparation.Grid.program_mem_uniform line 220
  18. theorem OAI.CPTSeparation.Grid.program_set_uniform line 224
  19. theorem OAI.CPTSeparation.Grid.program_pure line 231
  20. theorem OAI.CPTSeparation.Grid.program_input_definable line 239
  21. def OAI.CPTSeparation.Grid.twoCharges line 273
  22. theorem OAI.CPTSeparation.Grid.stage_sentence_agrees line 297
  23. lemma OAI.CPTSeparation.Quantitative.const_little_rpow line 335
  24. lemma OAI.CPTSeparation.Quantitative.power_little_power line 339
  25. lemma OAI.CPTSeparation.Quantitative.ceil_little line 348
  26. def OAI.CPTSeparation.Quantitative.radius line 361
  27. def OAI.CPTSeparation.Quantitative.palette line 363
  28. lemma OAI.CPTSeparation.Quantitative.log_volume_little line 365
  29. lemma OAI.CPTSeparation.Quantitative.radius_little line 375
  30. lemma OAI.CPTSeparation.Quantitative.radius_little_palette line 391
  31. lemma OAI.CPTSeparation.Quantitative.homogeneity_little line 395
  32. lemma OAI.CPTSeparation.Quantitative.floor_big line 414
  33. lemma OAI.CPTSeparation.Quantitative.giant_little line 420
  34. theorem OAI.CPTSeparation.Quantitative.eventual_bounds line 435
  35. def OAI.CPTSeparation.Quantitative.timeExponent line 462
  36. def OAI.CPTSeparation.Quantitative.traceExponent line 464
  37. lemma OAI.CPTSeparation.Quantitative.timeExponent_ge_two line 466
  38. lemma OAI.CPTSeparation.Quantitative.nat_le_power line 468
  39. lemma OAI.CPTSeparation.Quantitative.polynomial_bounds line 476
  40. lemma OAI.CPTSeparation.Quantitative.real_trace_bound line 502
  41. lemma OAI.CPTSeparation.Interpretations.Program.stage_le_cost line 515
  42. lemma OAI.CPTSeparation.Interpretations.Program.size_le_cost line 519
  43. lemma OAI.CPTSeparation.Grid.atomSizeConstant_pos line 533
  44. theorem OAI.CPTSeparation.Grid.exists_numeric_box line 537
  45. def OAI.CPTSeparation.structureQuery line 579
  46. theorem OAI.CPTSeparation.Grid.program_agrees_on_some_box line 586
  47. theorem OAI.CPTSeparation.query_not_interpretation_definable line 636