OAI/SetTheory/PartitionPrinciple/Forcing/NameMixingRanks.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.Name.nameRank line 12
  2. theorem OAI.PartitionPilot.Forcing.Name.eval_univ line 14
  3. theorem OAI.PartitionPilot.Forcing.Name.nameRank_eq line 25
  4. theorem OAI.PartitionPilot.Forcing.Name.entry_nameRank_lt line 31
  5. theorem OAI.PartitionPilot.Forcing.Name.nameRank_rename line 35
  6. theorem OAI.PartitionPilot.Forcing.Name.rank_eval_le line 41
  7. theorem OAI.PartitionPilot.Forcing.Name.nameRank_check line 49
  8. def OAI.PartitionPilot.Forcing.Name.selectName line 64
  9. theorem OAI.PartitionPilot.Forcing.Name.entry_selectName line 68
  10. theorem OAI.PartitionPilot.Forcing.Name.nameRank_selectName_le line 77
  11. theorem OAI.PartitionPilot.Forcing.PosetAction.act_selectName line 95
  12. def OAI.PartitionPilot.Forcing.Name.separationPredicate line 124
  13. def OAI.PartitionPilot.Forcing.Name.separationName line 128
  14. theorem OAI.PartitionPilot.Forcing.Name.entry_separationName line 131
  15. theorem OAI.PartitionPilot.Forcing.Name.eval_separationName line 138
  16. theorem OAI.PartitionPilot.Forcing.Name.nameRank_separationName_le line 165
  17. def OAI.PartitionPilot.Forcing.PosetAction.MixIndices line 180
  18. instance OAI.PartitionPilot.Forcing.PosetAction.mixIndices_small line 184
  19. def OAI.PartitionPilot.Forcing.PosetAction.mix line 189
  20. theorem OAI.PartitionPilot.Forcing.PosetAction.entry_mix line 193
  21. theorem OAI.PartitionPilot.Forcing.PosetAction.mix_entry_translated line 205
  22. theorem OAI.PartitionPilot.Forcing.PosetAction.mix_fixed line 218
  23. theorem OAI.PartitionPilot.Forcing.PosetAction.mix_hs line 234
  24. theorem OAI.PartitionPilot.Forcing.PosetAction.mem_eval_mix line 244
  25. theorem OAI.PartitionPilot.Forcing.PosetAction.eval_mix_of_active_equal line 264
  26. def OAI.PartitionPilot.Forcing.Name.UnionIndices line 291
  27. instance OAI.PartitionPilot.Forcing.Name.unionIndices_small line 295
  28. def OAI.PartitionPilot.Forcing.Name.unionName line 299
  29. theorem OAI.PartitionPilot.Forcing.Name.entry_unionName line 302
  30. theorem OAI.PartitionPilot.Forcing.Name.eval_unionName line 312
  31. theorem OAI.PartitionPilot.Forcing.Name.nameRank_unionName_le line 329
  32. theorem OAI.PartitionPilot.Forcing.PosetAction.act_unionName line 347
  33. theorem OAI.PartitionPilot.Forcing.PosetAction.unionName_hs line 368
  34. def OAI.PartitionPilot.Forcing.Name.envelope line 389
  35. theorem OAI.PartitionPilot.Forcing.Name.entry_envelope line 391
  36. theorem OAI.PartitionPilot.Forcing.Name.selectName_subset_envelope line 395
  37. theorem OAI.PartitionPilot.Forcing.Name.eval_mono line 403
  38. theorem OAI.PartitionPilot.Forcing.Name.eval_envelope line 409
  39. theorem OAI.PartitionPilot.Forcing.Name.separationName_true line 421
  40. theorem OAI.PartitionPilot.Forcing.Name.rename_mono line 433
  41. theorem OAI.PartitionPilot.Forcing.PosetAction.act_envelope line 449
  42. theorem OAI.PartitionPilot.Forcing.PosetAction.envelope_hs line 453
  43. theorem OAI.PartitionPilot.Forcing.PosetAction.act_subset_iff_fixed line 463
  44. theorem OAI.PartitionPilot.Forcing.PosetAction.nameRank_act line 488
  45. theorem OAI.PartitionPilot.Forcing.PosetAction.nameRank_mix_le line 492