OAI/SetTheory/PartitionPrinciple/Geometry/GroundContainmentOrders.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.PartialOrderCode.toPartialOrder line 14
  2. theorem OAI.PartitionPilot.Forcing.PartialOrderCode.conditionOrder_eq line 22
  3. def OAI.PartitionPilot.Forcing.PartialOrderCode.toOrderTop line 46
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.decoded_order_mem line 65
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_decoded_generic line 72
  6. def OAI.PartitionPilot.Forcing.reverseInclusionCode line 97
  7. theorem OAI.PartitionPilot.Forcing.mem_reverseInclusionCode line 100
  8. theorem OAI.PartitionPilot.Forcing.pair_mem_reverseInclusionCode line 106
  9. theorem OAI.PartitionPilot.Forcing.reverseInclusion_partialOrder line 116
  10. theorem OAI.PartitionPilot.Forcing.reverseInclusion_empty_top line 126
  11. def OAI.PartitionPilot.Forcing.BoundedFormula.subsetFormula line 134
  12. def OAI.PartitionPilot.Forcing.BoundedFormula.reverseInclusionEntryFormula line 136
  13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_subsetFormula line 139
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_reverseInclusionEntryFormula line 142
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.reverseInclusionCode_mem line 154