OAI/GroupTheory/PolycyclicRecognition/Algebra/BooleanPartitionMaps.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.booleanPartitionRefine line 13

   Source documentation

   Forget some of the Boolean coordinates of a realized partition cell.

   def booleanPartitionRefine {s t : Finset I} (h : s ⊆ t) :
       booleanPartitionCell a t → booleanPartitionCell a s := fun c =>
   …

   Mentions: OAI.PolycyclicRecognition.booleanPartitionCell

2. theorem OAI.PolycyclicRecognition.booleanPartitionRefine_point line 22
3. theorem OAI.PolycyclicRecognition.booleanPartitionRefine_surjective line 25
4. abbrev OAI.PolycyclicRecognition.booleanPartitionStage line 31
5. instance OAI.PolycyclicRecognition.booleanPartitionStage_projective line 34
6. def OAI.PolycyclicRecognition.booleanPartitionMap line 40

   Source documentation

   Pull a step function back to a finer partition.

   def booleanPartitionMap {s t : Finset I} (h : s ⊆ t) :
       booleanPartitionStage a s ⟶ booleanPartitionStage a t :=
   …

   Mentions: OAI.PolycyclicRecognition.booleanPartitionStage

7. def OAI.PolycyclicRecognition.booleanPartitionRetraction line 48

   Source documentation

   Choose one refined cell above each old cell to obtain a retraction.

   def booleanPartitionRetraction {s t : Finset I} (h : s ⊆ t) :
       booleanPartitionStage a t ⟶ booleanPartitionStage a s :=
   …

   Mentions: OAI.PolycyclicRecognition.booleanPartitionStage

8. theorem OAI.PolycyclicRecognition.booleanPartitionMap_retraction line 55
9. abbrev OAI.PolycyclicRecognition.booleanStepRepresentation line 64
10. def OAI.PolycyclicRecognition.booleanPartitionEvaluation line 66
11. theorem OAI.PolycyclicRecognition.booleanPartitionEvaluation_injective line 78
12. theorem OAI.PolycyclicRecognition.booleanPartitionMap_evaluation line 88