OAI/Computability/WitnessedChoice/SupportedForms.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WitnessedSeparation.Grid.boundary_eq_incidence line 14
  2. def OAI.WitnessedSeparation.Grid.GiantBound line 17
  3. theorem OAI.WitnessedSeparation.Grid.giant_exists_of_bound line 20
  4. theorem OAI.WitnessedSeparation.Grid.defect_transport line 35
  5. def OAI.WitnessedSeparation.Grid.CompatibleAssignment line 48
  6. theorem OAI.WitnessedSeparation.Grid.CompatibleAssignment.mono line 54
  7. theorem OAI.WitnessedSeparation.Grid.CompatibleAssignment.extend line 60
  8. theorem OAI.WitnessedSeparation.Grid.base_equivalence_numeric line 109
  9. inductive OAI.WitnessedSeparation.Forms.Form line 147
  10. def OAI.WitnessedSeparation.Forms.Form.value line 157
  11. theorem OAI.WitnessedSeparation.Forms.Form.value_atom line 166
  12. theorem OAI.WitnessedSeparation.Forms.Form.value_set_isSet line 170
  13. theorem OAI.WitnessedSeparation.Forms.Form.mem_value_set line 175
  14. theorem OAI.WitnessedSeparation.Forms.Form.value_iso line 186
  15. def OAI.WitnessedSeparation.Forms.cross31 line 222
  16. def OAI.WitnessedSeparation.Forms.cross42 line 226
  17. def OAI.WitnessedSeparation.Forms.cross34 line 230
  18. theorem OAI.WitnessedSeparation.Forms.swap_type line 234
  19. theorem OAI.WitnessedSeparation.Forms.elim_comp_cross31 line 246
  20. theorem OAI.WitnessedSeparation.Forms.elim_comp_cross42 line 250
  21. theorem OAI.WitnessedSeparation.Forms.elim_comp_cross34 line 254
  22. theorem OAI.WitnessedSeparation.Forms.set_subset_transfer line 274
  23. theorem OAI.WitnessedSeparation.Forms.set_eq_forward line 305
  24. theorem OAI.WitnessedSeparation.Forms.equality_transfer line 328
  25. theorem OAI.WitnessedSeparation.Forms.membership_forward line 365
  26. theorem OAI.WitnessedSeparation.Forms.membership_transfer line 389
  27. theorem OAI.WitnessedSeparation.Forms.value_smul line 414
  28. theorem OAI.WitnessedSeparation.Forms.value_supported line 420
  29. theorem OAI.WitnessedSeparation.Forms.hereditary_mem line 427
  30. theorem OAI.WitnessedSeparation.Forms.hereditary_intro line 434
  31. theorem OAI.WitnessedSeparation.Forms.value_hereditarily_supported line 444
  32. theorem OAI.WitnessedSeparation.Forms.smul_mem line 458
  33. theorem OAI.WitnessedSeparation.Forms.representation line 469
  34. def OAI.WitnessedSeparation.Counting.triangular line 530
  35. def OAI.WitnessedSeparation.Counting.snocTuple line 536
  36. theorem OAI.WitnessedSeparation.Counting.snocTuple_castSucc line 539
  37. theorem OAI.WitnessedSeparation.Counting.snocTuple_last line 542
  38. def OAI.WitnessedSeparation.Counting.snocEquiv line 545
  39. def OAI.WitnessedSeparation.Counting.appendPosition line 553
  40. theorem OAI.WitnessedSeparation.Counting.tupleType_append_one_bijection line 566
  41. theorem OAI.WitnessedSeparation.Counting.tupleType_append_fin_bijection line 617
  42. theorem OAI.WitnessedSeparation.Counting.tupleType_append_bijection line 678
  43. theorem OAI.WitnessedSeparation.Counting.tupleType_extension_equiv line 700
  44. theorem OAI.WitnessedSeparation.Forms.card_eq_mul_fiber line 724
  45. theorem OAI.WitnessedSeparation.Forms.card_eq_of_uniform_fibers line 734
  46. theorem OAI.WitnessedSeparation.Forms.range_card_mul_fiber line 748
  47. def OAI.WitnessedSeparation.Forms.Molecules line 774
  48. instance OAI.WitnessedSeparation.Forms.(instance at line 778) line 778
  49. def OAI.WitnessedSeparation.Forms.labelValues line 782
  50. instance OAI.WitnessedSeparation.Forms.(instance at line 787) line 787
  51. theorem OAI.WitnessedSeparation.Forms.mol_type_smul line 804
  52. def OAI.WitnessedSeparation.Forms.moleculesPerm line 815
  53. theorem OAI.WitnessedSeparation.Forms.uniform_value_fibers line 827
  54. theorem OAI.WitnessedSeparation.Forms.label_orbit line 851
  55. theorem OAI.WitnessedSeparation.Forms.label_smul_mem line 866
  56. theorem OAI.WitnessedSeparation.Forms.label_partition line 877
  57. def OAI.WitnessedSeparation.Forms.skipMiddle line 907
  58. def OAI.WitnessedSeparation.Forms.lastTwo line 910
  59. theorem OAI.WitnessedSeparation.Forms.elim_skipMiddle line 914
  60. theorem OAI.WitnessedSeparation.Forms.elim_lastTwo line 919
  61. theorem OAI.WitnessedSeparation.Forms.value_fiber_equiv line 928
  62. theorem OAI.WitnessedSeparation.Forms.label_overlap_transfer line 957
  63. theorem OAI.WitnessedSeparation.Forms.label_values_card line 979
  64. def OAI.WitnessedSeparation.cellSetoid line 1026
  65. theorem OAI.WitnessedSeparation.glue_finite_cells line 1029