OAI/SetTheory/PartitionPrinciple/Forcing/GroundSmallFunctionPermutations.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.TransitiveGround.smallFunctionOrder line 13
  2. def OAI.PartitionPilot.Forcing.TransitiveGround.smallFunctionTop line 18
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.smallFunction_le_iff line 25
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.smallFunction_raw_properties line 35
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.smallFunctionOrder_mem line 41
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_smallFunction_generic line 53
  7. theorem OAI.PartitionPilot.SetRealization.Presentation.relation_ext line 81
  8. theorem OAI.PartitionPilot.SetRealization.Presentation.graph_injection line 99
  9. theorem OAI.PartitionPilot.SetRealization.Presentation.converse_graph line 110
  10. def OAI.PartitionPilot.Forcing.graphRename line 127
  11. theorem OAI.PartitionPilot.Forcing.pair_mem_graphRename line 130
  12. theorem OAI.PartitionPilot.Forcing.graphRename_shape line 135
  13. theorem OAI.PartitionPilot.Forcing.graphRename_partial line 138
  14. theorem OAI.PartitionPilot.Forcing.graphRename_refl line 150
  15. theorem OAI.PartitionPilot.Forcing.graphRename_comp line 156
  16. theorem OAI.PartitionPilot.Forcing.graphRename_inverse line 163
  17. theorem OAI.PartitionPilot.Forcing.graphRename_mono line 172
  18. def OAI.PartitionPilot.Forcing.entryPermutationGraph line 178
  19. theorem OAI.PartitionPilot.Forcing.entryPermutation_injection line 181
  20. theorem OAI.PartitionPilot.Forcing.graphRename_eq_image line 191
  21. def OAI.PartitionPilot.Forcing.BoundedFormula.entryTransportFormula line 220
  22. def OAI.PartitionPilot.Forcing.BoundedFormula.entryPermutationFormula line 226
  23. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_entryTransportFormula line 230
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_entryPermutationFormula line 238
  25. theorem OAI.PartitionPilot.Forcing.BoundedFormula.entryPermutation_correct line 247
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.inverse_function_graph_mem line 278
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.entryPermutationGraph_mem line 287
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.graphRename_mem line 310
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.smallPartialFunctions_rename line 320
  30. def OAI.PartitionPilot.Forcing.TransitiveGround.renameSmallCondition line 353
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.raw_renameSmallCondition line 359
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.renameSmallCondition_inverse line 364
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.renameSmallCondition_le_iff line 374
  34. def OAI.PartitionPilot.Forcing.TransitiveGround.renameSmallOrderIso line 389
  35. theorem OAI.PartitionPilot.Forcing.TransitiveGround.raw_renameSmallOrderIso line 402