OAI/Geometry/HyperbolicGroups/SetoidGlue.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.PictureSwitch.glue line 14

   Source documentation

   Identifying two classes, without making any other identifications.

   def glue {D : Type*} (s : Setoid D) (a b : D) : Setoid D := by
   …

2. lemma OAI.HyperbolicObstruction.PictureSwitch.glue_iff line 21
3. lemma OAI.HyperbolicObstruction.PictureSwitch.le_glue line 29
4. lemma OAI.HyperbolicObstruction.PictureSwitch.glue_pair line 37
5. lemma OAI.HyperbolicObstruction.PictureSwitch.glue_le line 42
6. lemma OAI.HyperbolicObstruction.PictureSwitch.glue_eq_of_rel line 52
7. lemma OAI.HyperbolicObstruction.PictureSwitch.glue_monotone line 55
8. theorem OAI.HyperbolicObstruction.PictureSwitch.card_glue_of_not_rel line 62

   Source documentation

   Exactly one component is lost when previously distinct classes are glued.

   theorem card_glue_of_not_rel (h : ¬ s a b) :
       Nat.card (Quotient (glue s a b)) + 1 = Nat.card (Quotient s) := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.glue

9. theorem OAI.HyperbolicObstruction.PictureSwitch.card_glue line 91

   Source documentation

   A uniformly phrased count, including the already-related case.

   theorem card_glue : (Nat.card (Quotient (glue s a b)) : ℤ) =
       Nat.card (Quotient s) - if s a b then 0 else 1 := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.glue