OAI/SetTheory/PartitionPrinciple/Definability/MapFamilyApplicationGraphs.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.indexedRelationSection line 12
  2. theorem OAI.PartitionPilot.Forcing.indexedRelationSection_subset line 16
  3. theorem OAI.PartitionPilot.Forcing.mem_indexedRelationSection line 20
  4. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedRelationSection line 29
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.indexedRelationSectionEntryFormula line 49
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_indexedRelationSectionEntryFormula line 53
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.indexedRelationSectionFormula line 61
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_indexedRelationSectionFormula line 67
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.indexedRelationFamilyEntryFormula line 88
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_indexedRelationFamilyEntryFormula line 92
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedRelationSection_mem line 108
  12. def OAI.PartitionPilot.Forcing.TransitiveGround.indexedRelationSections line 128
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_indexedRelationSections line 133
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedRelationSections_mem line 144
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedRelationSections_function line 166
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedRelationSections_spec line 182
  17. def OAI.PartitionPilot.Forcing.indexedCarrierLabels line 213
  18. theorem OAI.PartitionPilot.Forcing.indexedCarrierLabels_subset line 217
  19. theorem OAI.PartitionPilot.Forcing.mem_indexedCarrierLabels line 221
  20. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedCarrierLabels line 232
  21. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedCarrierLabels_of_entry line 243
  22. def OAI.PartitionPilot.Forcing.BoundedFormula.indexedCarrierLabelFormula line 255
  23. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_indexedCarrierLabelFormula line 261
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedCarrierLabels_mem line 276
  25. def OAI.PartitionPilot.Forcing.mapFamilyApplicationGraph line 303
  26. theorem OAI.PartitionPilot.Forcing.pair_mem_mapFamilyApplicationGraph line 308
  27. def OAI.PartitionPilot.Forcing.BoundedFormula.mapFamilyApplicationEntryFormula line 323
  28. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mapFamilyApplicationEntryFormula line 329
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mapFamilyApplicationGraph_mem line 344