OAI/Geometry/HyperbolicGroups/Pinned.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PinnedAssignments.Free line 17
2. def OAI.HyperbolicObstruction.PinnedAssignments.extend line 19
3. lemma OAI.HyperbolicObstruction.PinnedAssignments.extend_free line 23
4. lemma OAI.HyperbolicObstruction.PinnedAssignments.extend_pin line 27
5. def OAI.HyperbolicObstruction.PinnedAssignments.support line 30
6. lemma OAI.HyperbolicObstruction.PinnedAssignments.mem_support line 32
7. lemma OAI.HyperbolicObstruction.PinnedAssignments.card_support line 35
8. lemma OAI.HyperbolicObstruction.PinnedAssignments.support_biUnion line 45
9. def OAI.HyperbolicObstruction.PinnedAssignments.Fieldwise line 52

   Source documentation

   Injectivity is imposed separately on each coordinate field, not globally.

   def Fieldwise (tag : W → F) (σ : W → A) : Prop :=
   …

10. instance OAI.HyperbolicObstruction.PinnedAssignments.(instance at line 55) line 55
11. def OAI.HyperbolicObstruction.PinnedAssignments.PinFieldwise line 58
12. def OAI.HyperbolicObstruction.PinnedAssignments.candidates line 61
13. lemma OAI.HyperbolicObstruction.PinnedAssignments.embedding_mem line 64
14. lemma OAI.HyperbolicObstruction.PinnedAssignments.candidates_lower line 80
15. lemma OAI.HyperbolicObstruction.PinnedAssignments.permutations line 91
16. lemma OAI.HyperbolicObstruction.PinnedAssignments.card_candidates_eq line 109