OAI/SetTheory/PartitionPrinciple/Model.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.PartitionPilot.Forcing.SetFormula line 9

   Also declared: ComparatorChallenges/PartitionPrinciple.lean:9 (same declaration text).

2. def OAI.PartitionPilot.Forcing.SetFormula.extend line 18

   Also declared: ComparatorChallenges/PartitionPrinciple.lean:18 (same declaration text).

3. def OAI.PartitionPilot.Forcing.SetFormula.Realize line 21

   Also declared: ComparatorChallenges/PartitionPrinciple.lean:21 (same declaration text).

4. def OAI.PartitionPilot.Forcing.SetFormula.ex line 28

   Also declared: ComparatorChallenges/PartitionPrinciple.lean:28 (same declaration text).

5. def OAI.PartitionPilot.Forcing.SetFormula.disj line 30

   Also declared: ComparatorChallenges/PartitionPrinciple.lean:30 (same declaration text).

6. def OAI.PartitionPilot.Forcing.SetFormula.imp line 32

   Also declared: ComparatorChallenges/PartitionPrinciple.lean:32 (same declaration text).

7. inductive OAI.PartitionPilot.Forcing.BoundedFormula line 36

   Also declared: ComparatorChallenges/PartitionPrinciple.lean:36 (same declaration text).

8. def OAI.PartitionPilot.Forcing.BoundedFormula.imp line 47

   Also declared: ComparatorChallenges/PartitionPrinciple.lean:47 (same declaration text).

9. def OAI.PartitionPilot.Forcing.BoundedFormula.disj line 49

   Also declared: ComparatorChallenges/PartitionPrinciple.lean:49 (same declaration text).

10. def OAI.PartitionPilot.Forcing.BoundedFormula.exMem line 51

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:51 (same declaration text).

11. def OAI.PartitionPilot.Forcing.BoundedFormula.toFormula line 54

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:54 (same declaration text).

12. def OAI.PartitionPilot.Forcing.BoundedFormula.singletonFormula line 61

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:61 (same declaration text).

13. def OAI.PartitionPilot.Forcing.BoundedFormula.unorderedPairFormula line 64

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:64 (same declaration text).

14. def OAI.PartitionPilot.Forcing.BoundedFormula.orderedPairFormula line 67

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:67 (same declaration text).

15. def OAI.PartitionPilot.Forcing.BoundedFormula.pairMembershipFormula line 72

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:72 (same declaration text).

16. def OAI.PartitionPilot.Forcing.BoundedFormula.relationBetweenFormula line 75

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:75 (same declaration text).

17. def OAI.PartitionPilot.Forcing.BoundedFormula.functionFormula line 78

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:78 (same declaration text).

18. def OAI.PartitionPilot.Forcing.BoundedFormula.nonemptyFormula line 83

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:83 (same declaration text).

19. def OAI.PartitionPilot.Forcing.BoundedFormula.choiceFunctionFormula line 85

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:85 (same declaration text).

20. structure OAI.PartitionPilot.Forcing.TransitiveGround line 92

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:92 (same declaration text).

21. structure OAI.PartitionPilot.Forcing.InjectionCode line 96

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:96 (same declaration text).

22. def OAI.PartitionPilot.Forcing.TransitiveGround.groundEmbeddable line 106

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:106 (same declaration text).

23. def OAI.PartitionPilot.Forcing.setTransitive line 110

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:110 (same declaration text).

24. def OAI.PartitionPilot.Forcing.ordinalSetProperty line 112

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:112 (same declaration text).

25. def OAI.PartitionPilot.Forcing.TransitiveGround.groundPower line 121

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:121 (same declaration text).

26. def OAI.PartitionPilot.Forcing.GroundBelow line 126

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:126 (same declaration text).

27. def OAI.PartitionPilot.Forcing.GroundCardinal line 129

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:129 (same declaration text).

28. def OAI.PartitionPilot.Forcing.CofinalFunctionCode line 132

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:132 (same declaration text).

29. def OAI.PartitionPilot.Forcing.GroundCofinalRegular line 136

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:136 (same declaration text).

30. def OAI.PartitionPilot.Forcing.GroundCardinalStrongLimit line 139

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:139 (same declaration text).

31. def OAI.PartitionPilot.Forcing.GroundStandardInaccessible line 142

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:142 (same declaration text).

32. def OAI.PartitionPilot.Forcing.SetFormula.extensionality line 148

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:148 (same declaration text).

33. def OAI.PartitionPilot.Forcing.SetFormula.foundation line 153

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:153 (same declaration text).

34. def OAI.PartitionPilot.Forcing.SetFormula.emptySet line 157

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:157 (same declaration text).

35. def OAI.PartitionPilot.Forcing.SetFormula.pairing line 159

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:159 (same declaration text).

36. def OAI.PartitionPilot.Forcing.SetFormula.union line 164

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:164 (same declaration text).

37. def OAI.PartitionPilot.Forcing.SetFormula.powerSet line 169

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:169 (same declaration text).

38. def OAI.PartitionPilot.Forcing.SetFormula.SeparationSchema line 174

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:174 (same declaration text).

39. def OAI.PartitionPilot.Forcing.SetFormula.CollectionSchema line 179

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:179 (same declaration text).

40. def OAI.PartitionPilot.Forcing.SetFormula.emptySetFormula line 186

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:186 (same declaration text).

41. def OAI.PartitionPilot.Forcing.SetFormula.successorFormula line 188

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:188 (same declaration text).

42. def OAI.PartitionPilot.Forcing.SetFormula.infinity line 192

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:192 (same declaration text).

43. def OAI.PartitionPilot.Forcing.SetFormula.choice line 196

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:196 (same declaration text).

44. def OAI.PartitionPilot.Forcing.SetFormula.ReplacementSchema line 200

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:200 (same declaration text).

45. def OAI.PartitionPilot.Forcing.SetFormula.finiteZFAxioms line 207

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:207 (same declaration text).

46. def OAI.PartitionPilot.Forcing.SetFormula.ZFRealization line 211

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:211 (same declaration text).

47. def OAI.PartitionPilot.Forcing.BoundedFormula.injectionFormula line 220

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:220 (same declaration text).

48. def OAI.PartitionPilot.Forcing.SetFormula.hasInjectionFormula line 229

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:229 (same declaration text).

49. def OAI.PartitionPilot.Forcing.BoundedFormula.surjectionFormula line 238

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:238 (same declaration text).

50. def OAI.PartitionPilot.Forcing.SetFormula.partitionPrinciple line 246

    Also declared: ComparatorChallenges/PartitionPrinciple.lean:246 (same declaration text).