OAI/AlgebraicGeometry/CharacterVarieties/Foundation/CutCircleIndex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IntegralCharacterVarieties.CutCircleIndex.extra line 14
  2. def OAI.IntegralCharacterVarieties.CutCircleIndex.count line 15
  3. abbrev OAI.IntegralCharacterVarieties.CutCircleIndex.Label line 16
  4. def OAI.IntegralCharacterVarieties.CutCircleIndex.selected line 17
  5. def OAI.IntegralCharacterVarieties.CutCircleIndex.oldPart line 37
  6. def OAI.IntegralCharacterVarieties.CutCircleIndex.enumeration line 43

    Source documentation

    Indexed boundary order: all old circles remain in their old order, the single mirror circle is appended at the selected parent, and every newly created strip disk has exactly one boundary.

    def enumeration : ((f : F ⊕ G) × Fin (count (G:=G) n p f)) ≃ Label (G:=G) n :=
…

    Mentions: OAI.IntegralCharacterVarieties.CutCircleIndex.count, OAI.IntegralCharacterVarieties.CutCircleIndex.Label

  7. lemma OAI.IntegralCharacterVarieties.CutCircleIndex.enumeration_old line 47
  8. lemma OAI.IntegralCharacterVarieties.CutCircleIndex.enumeration_mirror line 53
  9. lemma OAI.IntegralCharacterVarieties.CutCircleIndex.enumeration_fresh line 60