OAI/RingTheory/DirectFiniteness/BalanceRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.Planar.cycleSubtypeMap line 16

   Source documentation

   The inclusion of the cycles of an invariant subset.

   def cycleSubtypeMap (p : Perm α) (P : α → Prop) (hP : ∀ x, P (p x) ↔ P x) :
       Cycles (p.subtypePerm hP) → Cycles p :=
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.Cycles

2. lemma OAI.KaplanskyCounterexample.Planar.cycleSubtypeMap_injective line 21
3. lemma OAI.KaplanskyCounterexample.Planar.sum_cycle_subtype line 31
4. def OAI.KaplanskyCounterexample.Planar.WeakBalanced.restrict line 57

   Source documentation

   Discard components not containing the exception.

   def WeakBalanced.restrict (D : WeakBalanced R Inc ι) (P : α → Prop)
       (hb : ∀ x, P (R.black x) ↔ P x) (hw : ∀ x, P (R.white x) ↔ P x)
       (e : α) (he : cycleClass R.white e = D.exception) (hPe : P e) :
       WeakBalanced (R.restrict P hb hw) Inc ι where
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.WeakBalanced, OAI.KaplanskyCounterexample.Planar.cycleClass