OAI/SetTheory/PartitionPrinciple/Geometry/GroundTemplateIntervalFamilies.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.indexedAttachmentDomainEntryFormula line 17
  2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_indexedAttachmentDomainEntryFormula line 22
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.indexedAttachmentFreshEntryFormula line 31
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_indexedAttachmentFreshEntryFormula line 41
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.familyPointBound_mem line 58
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedAttachmentDomain_mem line 62
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedAttachmentFresh_mem line 83
  8. def OAI.PartitionPilot.Forcing.batchHeightEndpointRelation line 118
  9. theorem OAI.PartitionPilot.Forcing.pair_mem_batchHeightEndpointRelation line 131
  10. structure OAI.PartitionPilot.Forcing.BatchHeightEndpointCode line 159
  11. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.endpoint_base_entry line 181
  12. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchHeightEndpointRelation_total line 186
  13. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchHeightEndpointRelation_laws line 221
  14. theorem OAI.PartitionPilot.Forcing.BatchHeightEndpointCode.interval_upper line 254
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_intervalEmbedding_family line 279
  16. def OAI.PartitionPilot.Forcing.BoundedFormula.endpointRightTripleFormula line 332
  17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_endpointRightTripleFormula line 336
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.endpointRightMembershipFormula line 350
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_endpointRightMembershipFormula line 353
  20. def OAI.PartitionPilot.Forcing.BoundedFormula.endpointTupleFormula line 364
  21. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_endpointTupleFormula line 368
  22. def OAI.PartitionPilot.Forcing.BoundedFormula.batchHeightEndpointFormula line 384
  23. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_batchHeightEndpointFormula line 396
  24. def OAI.PartitionPilot.Forcing.endpointColumns line 411
  25. def OAI.PartitionPilot.Forcing.endpointPairs line 414
  26. def OAI.PartitionPilot.Forcing.endpointLows line 417
  27. def OAI.PartitionPilot.Forcing.endpointHighs line 420
  28. theorem OAI.PartitionPilot.Forcing.endpointProjection_functions line 423
  29. theorem OAI.PartitionPilot.Forcing.endpointProjection_entries line 433
  30. theorem OAI.PartitionPilot.Forcing.batchHeightEndpointCode_of_selection line 450
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchHeightEndpointRelation_mem line 492
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.endpointProjections_mem line 520
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_batchHeightEndpoints line 539
  34. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.intervalInputs line 576
  35. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_templateIntervalFamily line 598