OAI/SetTheory/PartitionPrinciple/Geometry/GroundHeightPushforward.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.SetRealization.Presentation.meetEmbeddingCode line 19
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyClassifier_entry_iff line 76
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyGeometry_spec line 84
  4. structure OAI.PartitionPilot.Forcing.IdealEmbeddingCode line 125
  5. theorem OAI.PartitionPilot.Forcing.IdealEmbeddingCode.order_iff line 137
  6. theorem OAI.PartitionPilot.Forcing.IdealEmbeddingCode.principal_iff line 143
  7. theorem OAI.PartitionPilot.Forcing.IdealEmbeddingCode.principal_range line 151
  8. theorem OAI.PartitionPilot.SetRealization.Presentation.idealEmbeddingCode line 174
  9. def OAI.PartitionPilot.Forcing.flatCopyEmbeddingGraph line 207
  10. theorem OAI.PartitionPilot.Forcing.pair_mem_flatCopyEmbeddingGraph line 211
  11. def OAI.PartitionPilot.Forcing.BoundedFormula.flatCopyEmbeddingEntryFormula line 224
  12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_flatCopyEmbeddingEntryFormula line 228
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyEmbeddingGraph_mem line 241
  14. theorem OAI.PartitionPilot.Forcing.flatCopyEmbeddingGraph_eq_graph line 270
  15. theorem OAI.PartitionPilot.Forcing.flatCopyEmbeddingGraph_code line 288
  16. def OAI.PartitionPilot.Forcing.pushedHeightGraph line 307
  17. theorem OAI.PartitionPilot.Forcing.pushedHeightGraph_entry line 310
  18. theorem OAI.PartitionPilot.Forcing.pushedHeightGraph_function line 326
  19. theorem OAI.PartitionPilot.Forcing.pushedHeightGraph_range line 331
  20. theorem OAI.PartitionPilot.Forcing.pushedHeightGraph_strictLex line 347
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pushedHeightGraph_mem line 365