OAI/SetTheory/PartitionPrinciple/Geometry/GroundCompressionStampBounds.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.compressionStamp line 9
  2. theorem OAI.PartitionPilot.Forcing.compressionStamp_zero line 13
  3. theorem OAI.PartitionPilot.Forcing.compressionStamp_succ line 16
  4. theorem OAI.PartitionPilot.Forcing.compressionStamp_subset line 19
  5. theorem OAI.PartitionPilot.Forcing.compressionStamp_mem_iff line 25
  6. theorem OAI.PartitionPilot.Forcing.compressionStamp_ordinal line 34
  7. theorem OAI.PartitionPilot.Forcing.compressionStamp_base_mem line 40
  8. theorem OAI.PartitionPilot.Forcing.compressionStamp_old_mem line 43
  9. theorem OAI.PartitionPilot.Forcing.compressionStamp_union_ordinal line 48
  10. structure OAI.PartitionPilot.Forcing.CompressionStampCode line 59
  11. theorem OAI.PartitionPilot.Forcing.CompressionStampCode.stamp_mem_limit line 69
  12. theorem OAI.PartitionPilot.Forcing.CompressionStampCode.stamp_ne_limit line 72
  13. theorem OAI.PartitionPilot.Forcing.CompressionStampCode.base_mem_limit line 76
  14. theorem OAI.PartitionPilot.Forcing.CompressionStampCode.value_ordinal line 78
  15. theorem OAI.PartitionPilot.Forcing.CompressionStampCode.entry_below_limit line 81
  16. theorem OAI.PartitionPilot.Forcing.mem_compressionStamp_iff line 92
  17. theorem OAI.PartitionPilot.Forcing.compressionStamp_not_old line 115
  18. theorem OAI.PartitionPilot.Forcing.old_ne_compressionStamp line 124
  19. theorem OAI.PartitionPilot.Forcing.compressionStamp_injective line 131
  20. theorem OAI.PartitionPilot.Forcing.CompressionStampCode.mem_limit_iff line 144
  21. def OAI.PartitionPilot.Forcing.FunctionGraphOn.natValue line 171
  22. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.natValue_entry line 174
  23. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.natValue_entry_iff line 178
  24. def OAI.PartitionPilot.Forcing.naturalFamilyUnion line 186
  25. theorem OAI.PartitionPilot.Forcing.naturalFamilyUnion_code line 189
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.naturalFamilyUnion_mem line 207
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_naturalStep_zero line 225
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_naturalStep_succ line 240
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.definableNaturalTrace_value line 275
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.definableNaturalStepClosure line 299
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_definableNaturalHistory line 332
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.compressionStamp_mem line 373
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundCompressionStamps line 382
  34. theorem OAI.PartitionPilot.Forcing.CompressionStampCode.function_into_bound line 432
  35. theorem OAI.PartitionPilot.Forcing.CompressionStampCode.successor_mem_limit line 440
  36. theorem OAI.PartitionPilot.Forcing.CompressionStampCode.rank_isLimit line 447
  37. theorem OAI.PartitionPilot.Forcing.GroundInaccessibleConditions.compressionStamp_mem line 470
  38. theorem OAI.PartitionPilot.Forcing.GroundInaccessibleConditions.compressionStamp_limit_mem line 476
  39. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundCompressionStamps_below line 500