OAI/SetTheory/PartitionConsistency/Forcing/RelationCalculus.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

RelationTools

  1. structure OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UnaryRelation line 18

    Source documentation

    An equality-invariant regular forcing predicate, used only to produce bounded HS subnames by literal collection.

    structure UnaryRelation where
…
  2. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UnaryRelation.test line 30
  3. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UnaryRelation.test_permute line 35
  4. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UnaryRelation.select line 51

    Source documentation

    The subset is formed from literal children of the bounding name.

    def select : S.Name :=
…
  5. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UnaryRelation.select_fixed line 56
  6. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.UnaryRelation.mem_select line 61
  7. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.bounded line 91

    Source documentation

    Bounds are included in the relation when proving uniqueness, so no functional behavior outside the specified sets is required.

    def bounded (X Y : S.Name) : S.BinaryRelation where
…
  8. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.inverse line 101
  9. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.comp line 109

    Source documentation

    Composition is the regular existential relation, not an external composition of selected evaluations.

    def comp (Q : S.BinaryRelation) : S.BinaryRelation where
…
  10. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.appRelation line 130

    Source documentation

    The application relation of a particular graph name.

    def appRelation (f : S.Name) : S.BinaryRelation where
…
  11. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mapsTo_function line 143

    Source documentation

    Convenient semantic consequences of the full internal function formulas.

    theorem mapsTo_function {f X Y : S.Name} {p : P}
    (h : S.Forces ![f,X,Y] p (SetLanguage.mapsTo 0 1 2)) :
    S.Forces ![f,X] p (SetLanguage.functionOn 0 1) := (S.forces_mapsTo _ _ _ _ _).mp h |>.1

    Mentions: OAI.PartitionConsistency.SetLanguage.mapsTo, OAI.PartitionConsistency.SetLanguage.functionOn

  12. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mapsTo_value line 147
  13. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mapsTo_total line 152
  14. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mapsTo_unique line 161
  15. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.surjection_mapsTo line 168
  16. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.surjection_onto line 172
  17. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.injection_mapsTo line 178
  18. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.injection_one line 182
  19. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.boundedApp line 200
  20. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.boundedApp_move line 202
  21. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.compositionRelation line 212
  22. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.compositionRelation_move line 215
  23. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.compositionGraph line 226
  24. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.app_compositionGraph line 235
  25. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.compositionRelation_one line 251
  26. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.compositionGraph_mapsTo line 269
  27. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.compositionGraph_surjection line 284
  28. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.compositionGraph_injection line 299
  29. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.inverseGraph line 317
  30. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.app_inverseGraph line 325
  31. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.inverseGraph_injection line 333
  32. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.inverseGraph_surjection line 347
  33. def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.restrictionGraph line 360

    Source documentation

    Restriction is a bounded application graph, not a change of interpretation of an old function name.

    def restrictionGraph (f X Y : S.Name) : S.Name :=
…
  34. theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.app_restrictionGraph line 368