OAI/ModelTheory/Choiceless/Forms.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CPTSeparation.Forms.card_eq_mul_fiber line 13
  2. theorem OAI.CPTSeparation.Forms.card_eq_of_uniform_fibers line 23
  3. theorem OAI.CPTSeparation.Forms.range_card_mul_fiber line 37
  4. def OAI.CPTSeparation.Forms.Molecules line 63
  5. instance OAI.CPTSeparation.Forms.(instance at line 67) line 67
  6. def OAI.CPTSeparation.Forms.labelValues line 71
  7. instance OAI.CPTSeparation.Forms.(instance at line 76) line 76
  8. theorem OAI.CPTSeparation.Forms.mol_type_smul line 92
  9. def OAI.CPTSeparation.Forms.moleculesPerm line 120
  10. theorem OAI.CPTSeparation.Forms.uniform_value_fibers line 131
  11. theorem OAI.CPTSeparation.Forms.label_orbit line 173
  12. theorem OAI.CPTSeparation.Forms.label_smul_mem line 206
  13. theorem OAI.CPTSeparation.Forms.label_partition line 234
  14. def OAI.CPTSeparation.Forms.skipMiddle line 263
  15. def OAI.CPTSeparation.Forms.lastTwo line 266
  16. theorem OAI.CPTSeparation.Forms.elim_skipMiddle line 270
  17. theorem OAI.CPTSeparation.Forms.elim_lastTwo line 281
  18. theorem OAI.CPTSeparation.Forms.value_fiber_equiv line 293
  19. theorem OAI.CPTSeparation.Forms.label_overlap_transfer line 321
  20. theorem OAI.CPTSeparation.Forms.label_values_card line 341
  21. def OAI.CPTSeparation.cellSetoid line 381
  22. theorem OAI.CPTSeparation.glue_finite_cells line 384
  23. abbrev OAI.CPTSeparation.Forms.Domain line 446
  24. def OAI.CPTSeparation.Forms.Cell line 449
  25. def OAI.CPTSeparation.Forms.cellEquiv line 466
  26. theorem OAI.CPTSeparation.Forms.cell_finite line 475
  27. theorem OAI.CPTSeparation.Forms.supported_domain_bijection line 482
  28. inductive OAI.CPTSeparation.Forms.HFRelation line 581
  29. def OAI.CPTSeparation.Forms.hfStructure line 584
  30. def OAI.CPTSeparation.Forms.Represented line 590
  31. def OAI.CPTSeparation.Forms.twoBlocks line 599
  32. theorem OAI.CPTSeparation.Forms.comp_twoBlocks line 610
  33. def OAI.CPTSeparation.Forms.splitBlock line 621
  34. theorem OAI.CPTSeparation.Forms.represented_equal line 642
  35. theorem OAI.CPTSeparation.Forms.represented_mem line 653
  36. theorem OAI.CPTSeparation.Forms.represented_atom line 666
  37. theorem OAI.CPTSeparation.Forms.base_value line 697
  38. theorem OAI.CPTSeparation.Forms.represented_base line 721
  39. theorem OAI.CPTSeparation.Forms.splitBlock_symm_new line 766
  40. theorem OAI.CPTSeparation.Forms.splitBlock_symm_old line 774
  41. theorem OAI.CPTSeparation.Forms.homogeneity_reindex line 782
  42. theorem OAI.CPTSeparation.Forms.represented_extension line 810
  43. theorem OAI.CPTSeparation.Forms.supported_eval_transfer line 859
  44. theorem OAI.CPTSeparation.Forms.supported_sentences_transfer line 885
  45. def OAI.CPTSeparation.Forms.namesOfCard line 922
  46. def OAI.CPTSeparation.Forms.HomogeneousThrough line 925
  47. theorem OAI.CPTSeparation.Forms.homogeneous_tuple line 931
  48. theorem OAI.CPTSeparation.Forms.hf_transfer line 943
  49. theorem OAI.CPTSeparation.Hereditary.supports_pad line 977
  50. theorem OAI.CPTSeparation.Grid.central_smul_HF line 998
  51. theorem OAI.CPTSeparation.Grid.small_orbit_supported line 1001
  52. theorem OAI.CPTSeparation.Grid.orbit_card_le_invariant_family line 1016
  53. theorem OAI.CPTSeparation.Grid.invariant_family_hereditarily_supported line 1028
  54. theorem OAI.CPTSeparation.Grid.atom_nonempty line 1050
  55. instance OAI.CPTSeparation.Grid.atom_nonempty_succ line 1053
  56. theorem OAI.CPTSeparation.Grid.central_analysis_isomorphism line 1055
  57. theorem OAI.CPTSeparation.Grid.homogeneous_through_numeric line 1059
  58. theorem OAI.CPTSeparation.Grid.base_empty_type line 1071
  59. theorem OAI.CPTSeparation.Grid.grid_hf_transfer line 1084