OAI/SetTheory/PartitionPrinciple/Forcing/GroundOrdinaryMembershipAntichainFamilies.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.antichainEligible_mem line 13
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.greedyAntichainStep_exists_unique line 31
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_greedyAntichainTrace line 56
  4. theorem OAI.PartitionPilot.Forcing.greedyAntichainTrace_relativeMaximal line 101
  5. theorem OAI.PartitionPilot.Forcing.RelativeMaximalAntichainCode.predense line 120
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundRelativeMaximalAntichain line 134
  7. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_ordinaryMembershipDecisions line 165
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryMembershipDecisions_mem line 178
  9. def OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryMembershipDecisionFamily line 185
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_ordinaryMembershipDecisionFamily line 189
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryMembershipDecisionFamily_mem line 200
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryMembershipDecisionFamily_function line 209
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ordinaryMembershipDecisionFamily_dense line 232
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_relativeMaximalAntichainFamily line 256
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_smallRelativeAntichainFamily line 302
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_ordinaryMembershipAntichainFamily line 343