OAI/SetTheory/PartitionPrinciple/Forcing/EvaluatedDomains.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PartitionPilot.Forcing.IsName line 16
  2. def OAI.PartitionPilot.Forcing.Name line 20
  3. def OAI.PartitionPilot.Forcing.Name.Entry line 25
  4. theorem OAI.PartitionPilot.Forcing.Name.entries_cover line 28
  5. theorem OAI.PartitionPilot.Forcing.Name.ext line 36
  6. theorem OAI.PartitionPilot.Forcing.Name.entry_rank_lt line 48
  7. theorem OAI.PartitionPilot.Forcing.Name.inductionOn line 56
  8. def OAI.PartitionPilot.Forcing.Name.Entries line 62
  9. instance OAI.PartitionPilot.Forcing.Name.entries_small line 64
  10. def OAI.PartitionPilot.Forcing.Name.assemble line 73
  11. theorem OAI.PartitionPilot.Forcing.Name.entry_assemble line 85
  12. theorem OAI.PartitionPilot.Forcing.Name.assemble_entries line 97
  13. def OAI.PartitionPilot.Forcing.Name.empty line 108
  14. theorem OAI.PartitionPilot.Forcing.Name.not_entry_empty line 112
  15. def OAI.PartitionPilot.Forcing.Name.eval line 126
  16. theorem OAI.PartitionPilot.Forcing.Name.mem_eval line 131
  17. theorem OAI.PartitionPilot.Forcing.Name.mem_eval_assemble line 140
  18. theorem OAI.PartitionPilot.Forcing.Name.eval_assemble line 153
  19. theorem OAI.PartitionPilot.Forcing.Name.eval_empty line 166
  20. theorem OAI.PartitionPilot.Forcing.Name.eval_empty_conditions line 175
  21. def OAI.PartitionPilot.Forcing.Name.ForcesEq line 194
  22. theorem OAI.PartitionPilot.Forcing.Name.forcesEq_mono line 202
  23. theorem OAI.PartitionPilot.Forcing.Name.forcesEq_refl line 208
  24. theorem OAI.PartitionPilot.Forcing.Name.forcesEq_symm line 218
  25. theorem OAI.PartitionPilot.Forcing.Name.forcesEq_of_dense line 230
  26. def OAI.PartitionPilot.Forcing.Name.MemWitness line 247
  27. def OAI.PartitionPilot.Forcing.Name.ForcesMem line 250
  28. theorem OAI.PartitionPilot.Forcing.Name.forcesMem_mono line 252
  29. theorem OAI.PartitionPilot.Forcing.Name.forcesMem_of_witness line 255
  30. theorem OAI.PartitionPilot.Forcing.Name.forcesMem_entry line 261
  31. theorem OAI.PartitionPilot.Forcing.Name.forcesMem_of_dense line 264
  32. theorem OAI.PartitionPilot.Forcing.Name.forcesEq_left line 271
  33. theorem OAI.PartitionPilot.Forcing.Name.forcesEq_right line 278
  34. theorem OAI.PartitionPilot.Forcing.Name.forcesEq_iff line 282
  35. def OAI.PartitionPilot.Forcing.Name.check line 308
  36. theorem OAI.PartitionPilot.Forcing.Name.entry_check line 313
  37. theorem OAI.PartitionPilot.Forcing.Name.eval_check line 322
  38. theorem OAI.PartitionPilot.Forcing.Name.check_injective line 337
  39. def OAI.PartitionPilot.Forcing.Name.singleton line 343
  40. def OAI.PartitionPilot.Forcing.Name.unorderedPair line 346
  41. def OAI.PartitionPilot.Forcing.Name.orderedPair line 349
  42. theorem OAI.PartitionPilot.Forcing.Name.eval_singleton line 352
  43. theorem OAI.PartitionPilot.Forcing.Name.eval_unorderedPair line 363
  44. theorem OAI.PartitionPilot.Forcing.Name.eval_orderedPair line 377
  45. structure OAI.PartitionPilot.Forcing.Name.NameDomain line 393
  46. def OAI.PartitionPilot.Forcing.Name.ForcesNotMem line 397
  47. theorem OAI.PartitionPilot.Forcing.Name.not_forcesMem_refine line 400
  48. def OAI.PartitionPilot.Forcing.Name.EqDecisionWitness line 411
  49. theorem OAI.PartitionPilot.Forcing.Name.eqDecisionWitness_dense line 416
  50. def OAI.PartitionPilot.Forcing.Name.atomicFamily line 432
  51. theorem OAI.PartitionPilot.Forcing.Name.generic_mem_witness line 436
  52. def OAI.PartitionPilot.Forcing.Name.NameDomain.values line 452
  53. theorem OAI.PartitionPilot.Forcing.Name.NameDomain.mem_values line 455
  54. theorem OAI.PartitionPilot.Forcing.Name.NameDomain.values_transitive line 463
  55. theorem OAI.PartitionPilot.Forcing.Name.NameDomain.values_extensionality line 469
  56. theorem OAI.PartitionPilot.Forcing.Name.NameDomain.values_foundation line 480