OAI/ModelTheory/Categoricity/Partition.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CHObstruction.EndHomogeneous.residual line 19
  2. def OAI.CHObstruction.EndHomogeneous.step line 25
  3. def OAI.CHObstruction.EndHomogeneous.rep line 29
  4. theorem OAI.CHObstruction.EndHomogeneous.rep_eq line 31
  5. theorem OAI.CHObstruction.EndHomogeneous.active line 35
  6. theorem OAI.CHObstruction.EndHomogeneous.lt_of_no_stop line 49
  7. def OAI.CHObstruction.EndHomogeneous.Stops line 58
  8. def OAI.CHObstruction.EndHomogeneous.first line 60
  9. theorem OAI.CHObstruction.EndHomogeneous.first_eq line 63
  10. theorem OAI.CHObstruction.EndHomogeneous.before_first line 66
  11. def OAI.CHObstruction.EndHomogeneous.profile line 72
  12. theorem OAI.CHObstruction.EndHomogeneous.equal_reps line 74
  13. def OAI.CHObstruction.EndHomogeneous.stopCode line 120
  14. theorem OAI.CHObstruction.EndHomogeneous.stopCode_injective line 123
  15. theorem OAI.CHObstruction.EndHomogeneous.exists_sequence line 136
  16. def OAI.CHObstruction.FinitePartition.Constant line 164
  17. def OAI.CHObstruction.FinitePartition.Homogeneous line 167
  18. theorem OAI.CHObstruction.FinitePartition.arity_step line 170
  19. theorem OAI.CHObstruction.FinitePartition.power_lt line 215
  20. theorem OAI.CHObstruction.FinitePartition.estimate line 221
  21. def OAI.CHObstruction.ThresholdArithmetic.ξ line 267
  22. theorem OAI.CHObstruction.ThresholdArithmetic.palette_infinite line 269
  23. theorem OAI.CHObstruction.ThresholdArithmetic.palette_lt line 272
  24. theorem OAI.CHObstruction.ThresholdArithmetic.index_limit line 275
  25. theorem OAI.CHObstruction.ThresholdArithmetic.strongLimit line 278
  26. theorem OAI.CHObstruction.ThresholdArithmetic.cofinality line 281
  27. theorem OAI.CHObstruction.ThresholdArithmetic.palette_lt_cofinality line 286
  28. theorem OAI.CHObstruction.ThresholdArithmetic.endpoint_eq_hanf line 290
  29. theorem OAI.CHObstruction.FinitePartition.Constant.mono line 302
  30. theorem OAI.CHObstruction.FinitePartition.Constant.image line 306
  31. theorem OAI.CHObstruction.FinitePartition.inside line 321
  32. def OAI.CHObstruction.FinitePatterns.Prefix line 348
  33. def OAI.CHObstruction.FinitePatterns.Unbounded line 351
  34. theorem OAI.CHObstruction.FinitePatterns.extend line 359
  35. theorem OAI.CHObstruction.FinitePatterns.initial line 391
  36. def OAI.CHObstruction.FinitePatterns.states line 398
  37. def OAI.CHObstruction.FinitePatterns.colors line 405
  38. theorem OAI.CHObstruction.FinitePatterns.states_agree line 407
  39. theorem OAI.CHObstruction.FinitePatterns.colors_unbounded line 419
  40. theorem OAI.CHObstruction.FinitePatterns.exists_patterns line 430