OAI/SetTheory/PartitionPrinciple/Forcing/FinitePrincipalNameSupports.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.Name.isName_of_subset line 12
  2. def OAI.PartitionPilot.Forcing.Name.ofSubset line 23
  3. theorem OAI.PartitionPilot.Forcing.Name.ofSubset_code line 27
  4. theorem OAI.PartitionPilot.Forcing.Name.entry_ofSubset line 30
  5. theorem OAI.PartitionPilot.Forcing.Name.entry_term_of_subset line 34
  6. theorem OAI.PartitionPilot.Forcing.Name.act_subset_of_closed line 38
  7. def OAI.PartitionPilot.Forcing.Name.crossStageMembershipCode line 61
  8. theorem OAI.PartitionPilot.Forcing.Name.crossStageMembershipCode_subset line 67
  9. theorem OAI.PartitionPilot.Forcing.Name.pair_mem_crossStageMembershipCode line 71
  10. theorem OAI.PartitionPilot.Forcing.Name.crossStageMembershipCode_isName line 85
  11. def OAI.PartitionPilot.Forcing.Name.crossStageMembershipName line 89
  12. theorem OAI.PartitionPilot.Forcing.Name.crossStageMembershipName_val line 94
  13. theorem OAI.PartitionPilot.Forcing.Name.entry_crossStageMembershipName line 98
  14. theorem OAI.PartitionPilot.Forcing.SetFormula.forces_nonempty_iff_dense_activeTerms line 113
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.crossStageMembershipCode_eq_selection line 151
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.crossStageMembershipCode_mem line 179
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.crossStageMembershipName_mem line 189
  18. theorem OAI.PartitionPilot.Forcing.PosetAction.point_inv_left line 204
  19. theorem OAI.PartitionPilot.Forcing.PosetAction.point_inv_right line 207
  20. def OAI.PartitionPilot.Forcing.PosetAction.principalFix line 210
  21. theorem OAI.PartitionPilot.Forcing.PosetAction.principalFix_antitone line 218
  22. theorem OAI.PartitionPilot.Forcing.PosetAction.principalFix_conjugation line 221
  23. def OAI.PartitionPilot.Forcing.PosetAction.PrincipalSupported line 237
  24. theorem OAI.PartitionPilot.Forcing.PosetAction.principalSupported_top line 239
  25. theorem OAI.PartitionPilot.Forcing.PosetAction.principalSupported_upward line 241
  26. theorem OAI.PartitionPilot.Forcing.PosetAction.principalSupported_inf line 246
  27. theorem OAI.PartitionPilot.Forcing.PosetAction.principalSupported_conjugate line 255
  28. def OAI.PartitionPilot.Forcing.PosetAction.principalSupportFamily line 265
  29. theorem OAI.PartitionPilot.Forcing.PosetAction.principalSupportFamily_basis line 273
  30. theorem OAI.PartitionPilot.Forcing.Name.exists_commonPrincipalNameSupport line 284
  31. def OAI.PartitionPilot.Forcing.NiceNameCode line 306
  32. theorem OAI.PartitionPilot.Forcing.niceNameCode_iff line 312
  33. theorem OAI.PartitionPilot.Forcing.niceNameCode_ofSubset_iff line 322
  34. theorem OAI.PartitionPilot.Forcing.niceNameCode_isName line 330
  35. theorem OAI.PartitionPilot.Forcing.niceNameCode_subset line 335
  36. theorem OAI.PartitionPilot.Forcing.niceNameCode_hs line 340
  37. theorem OAI.PartitionPilot.Forcing.niceNameCode_conjugate line 348
  38. theorem OAI.PartitionPilot.Forcing.niceNameCode_act_iff line 360
  39. theorem OAI.PartitionPilot.Forcing.principalFix_map_conjugate line 384
  40. theorem OAI.PartitionPilot.Forcing.niceNameCode_principal_hs line 398
  41. theorem OAI.PartitionPilot.Forcing.niceNameCode_principal_act_iff line 406
  42. def OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidates line 424
  43. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_niceNameCandidates line 427
  44. theorem OAI.PartitionPilot.Forcing.TransitiveGround.name_mem_niceNameCandidates line 435
  45. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidates_subset line 447
  46. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceNameCandidates_mem line 452