OAI/SetTheory/PartitionPrinciple/Geometry/GroundPreparedAlignedReferenceCollisions.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.SynchronizedEnumerationCode.codomain_mono line 11
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparedCertificateCode_of_selected line 34
  3. def OAI.PartitionPilot.Forcing.TransitiveGround.TypedPreparedCertificate line 89
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparedCertificateCode_typed line 99
  5. theorem OAI.PartitionPilot.Forcing.PreparedCertificateFamilyCode.bounds_mono line 158
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparedCertificateFamilyCode_of_selected line 178
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.anchor_of_dataBound line 226

    Also declared: OAI/SetTheory/PartitionPrinciple/Geometry/GroundPreparedStructuralInsertionCollisions.lean:129 (same declaration text).

  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignment_aligned_reference line 259
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralAssignment_prepared_aligned_collision line 411