OAI/SetTheory/PartitionPrinciple/Geometry/TemplateHeightRangeCodes.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs line 12
  2. def OAI.PartitionPilot.Forcing.componentHeightGraph line 25
  3. theorem OAI.PartitionPilot.Forcing.componentHeightGraph_shape line 33
  4. theorem OAI.PartitionPilot.Forcing.pair_mem_componentHeightGraph line 38
  5. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.componentHeightGraph_entry_iff line 65
  6. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.componentHeightGraph_function line 82
  7. def OAI.PartitionPilot.Forcing.taggedHeightGraph line 111
  8. theorem OAI.PartitionPilot.Forcing.taggedHeightGraph_old_entry line 116
  9. theorem OAI.PartitionPilot.Forcing.taggedHeightGraph_fresh_entry line 126
  10. theorem OAI.PartitionPilot.Forcing.taggedHeightGraph_function line 143
  11. def OAI.PartitionPilot.Forcing.heightOrderRestriction line 161
  12. theorem OAI.PartitionPilot.Forcing.pair_mem_heightOrderRestriction line 164
  13. theorem OAI.PartitionPilot.Forcing.heightOrderRestriction_linear line 169
  14. theorem OAI.PartitionPilot.Forcing.function_on_relationImage line 185
  15. def OAI.PartitionPilot.Forcing.heightImageCandidate line 192
  16. def OAI.PartitionPilot.Forcing.heightOrderCandidate line 197
  17. def OAI.PartitionPilot.Forcing.heightImageFamily line 201
  18. def OAI.PartitionPilot.Forcing.heightOrderFamily line 205
  19. theorem OAI.PartitionPilot.Forcing.pair_mem_heightImageFamily line 209
  20. theorem OAI.PartitionPilot.Forcing.pair_mem_heightOrderFamily line 220
  21. def OAI.PartitionPilot.Forcing.BoundedFormula.heightImageEquationFormula line 235
  22. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_heightImageEquationFormula line 239
  23. def OAI.PartitionPilot.Forcing.BoundedFormula.heightOrderEquationFormula line 258
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_heightOrderEquationFormula line 262
  25. def OAI.PartitionPilot.Forcing.BoundedFormula.heightImageCandidateFormula line 282
  26. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_heightImageCandidateFormula line 290
  27. def OAI.PartitionPilot.Forcing.BoundedFormula.heightOrderCandidateFormula line 303
  28. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_heightOrderCandidateFormula line 309
  29. def OAI.PartitionPilot.Forcing.BoundedFormula.heightImageFamilyEntryFormula line 322
  30. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_heightImageFamilyEntryFormula line 327
  31. def OAI.PartitionPilot.Forcing.BoundedFormula.heightOrderFamilyEntryFormula line 346
  32. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_heightOrderFamilyEntryFormula line 350