OAI/SetTheory/PartitionPrinciple/Geometry/IntervalEmbeddingFamilyCodes.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.leastInjectionMember line 13
  2. theorem OAI.PartitionPilot.Forcing.leastInjectionMember_unique line 17
  3. theorem OAI.PartitionPilot.Forcing.leastInjectionMember_exists_unique line 30
  4. def OAI.PartitionPilot.Forcing.canonicalEnumerationDefault line 50
  5. theorem OAI.PartitionPilot.Forcing.canonicalEnumerationDefault_least line 54
  6. theorem OAI.PartitionPilot.Forcing.canonicalEnumerationDefault_eq line 61
  7. def OAI.PartitionPilot.Forcing.canonicalEnumeration line 66
  8. theorem OAI.PartitionPilot.Forcing.canonicalEnumeration_eq_of_least line 69
  9. theorem OAI.PartitionPilot.Forcing.canonicalEnumeration_isFunc line 74
  10. theorem OAI.PartitionPilot.Forcing.canonicalEnumeration_onto line 79
  11. theorem OAI.PartitionPilot.Forcing.canonicalEnumeration_unique line 84
  12. def OAI.PartitionPilot.Forcing.BoundedFormula.leastInjectionMemberFormula line 91
  13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_leastInjectionMemberFormula line 96
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.canonicalEnumerationDefault_mem line 113
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.canonicalEnumeration_mem line 118
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.canonicalEnumeration_spec line 128
  17. def OAI.PartitionPilot.Forcing.intervalSequenceGraph line 155
  18. theorem OAI.PartitionPilot.Forcing.intervalSequenceGraph_subset line 160
  19. theorem OAI.PartitionPilot.Forcing.mem_intervalSequenceGraph line 164
  20. theorem OAI.PartitionPilot.Forcing.pair_mem_intervalSequenceGraph line 173
  21. theorem OAI.PartitionPilot.Forcing.intervalSequenceGraph_isFunc line 184
  22. theorem OAI.PartitionPilot.Forcing.intervalSequenceGraph_injection line 198
  23. theorem OAI.PartitionPilot.Forcing.intervalSequenceGraph_order_iff line 208
  24. theorem OAI.PartitionPilot.Forcing.intervalSequenceGraph_inside line 217
  25. theorem OAI.PartitionPilot.Forcing.intervalSequenceGraph_sequence_entry line 224
  26. def OAI.PartitionPilot.Forcing.BoundedFormula.intervalSequenceEntryFormula line 242
  27. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_intervalSequenceEntryFormula line 248
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.intervalSequenceGraph_mem line 264
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.intervalSequenceDescent_spec line 286
  30. structure OAI.PartitionPilot.Forcing.IntervalEmbeddingCode line 317
  31. theorem OAI.PartitionPilot.Forcing.intervalEmbeddingCode_empty line 323
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_intervalEmbedding_of_enumeration line 337
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_intervalEmbedding line 359
  34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundRationalIntervals line 386
  35. structure OAI.PartitionPilot.Forcing.IntervalEmbeddingFamilyInputs line 416
  36. def OAI.PartitionPilot.Forcing.intervalEmbeddingCandidate line 426
  37. def OAI.PartitionPilot.Forcing.intervalEmbeddingRelation line 432
  38. theorem OAI.PartitionPilot.Forcing.pair_mem_intervalEmbeddingRelation line 436
  39. theorem OAI.PartitionPilot.Forcing.IntervalEmbeddingFamilyInputs.candidate_iff line 452
  40. theorem OAI.PartitionPilot.Forcing.IntervalEmbeddingFamilyInputs.embedding_subset_bound line 471