OAI/Geometry/HyperbolicGroups/ExtensionMargin.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HyperbolicObstruction.StarModel.ExtPos line 17
  2. def OAI.HyperbolicObstruction.StarModel.extPos line 20
  3. lemma OAI.HyperbolicObstruction.StarModel.extPos_injective line 25
  4. def OAI.HyperbolicObstruction.StarModel.branchPins line 32

    Source documentation

    All fields belonging to the specified branch are fixed in an extension.

    def branchPins (U : Finset F) (jā‚€ : B) : Finset (Var (B := B) U) :=
ā€¦

    Mentions: OAI.HyperbolicObstruction.StarModel.Var

  5. lemma OAI.HyperbolicObstruction.StarModel.mem_branchPins_inl line 36
  6. lemma OAI.HyperbolicObstruction.StarModel.mem_branchPins_inr line 41
  7. lemma OAI.HyperbolicObstruction.StarModel.extension_free_card line 52
  8. lemma OAI.HyperbolicObstruction.StarModel.extension_active line 109
  9. lemma OAI.HyperbolicObstruction.StarModel.extension_selected_cost line 121
  10. lemma OAI.HyperbolicObstruction.StarModel.extension_critical_gap line 152