OAI/RingTheory/DirectFiniteness/EulerBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.Planar.quotient_card_antitone line 15
2. def OAI.KaplanskyCounterexample.Planar.Ribbon.components line 22

   Source documentation

   Connected components of a bipartite rotation system, including edge components consisting of a single edge. Isolated vertices are not encoded.

   def Ribbon.components (R : Ribbon α) : Setoid α :=
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.Ribbon

3. lemma OAI.KaplanskyCounterexample.Planar.cycles_inv_card line 26
4. theorem OAI.KaplanskyCounterexample.Planar.Ribbon.euler_le line 36

   Source documentation

   The elementary genus inequality for an arbitrary finite ribbon system. This supplies the topological constraint needed when components are discarded in the planar minimality argument; it is not assumed as an extra hypothesis.

   theorem Ribbon.euler_le (R : Ribbon α) :
       Nat.card (Cycles R.black) + Nat.card (Cycles R.white) + Nat.card (Cycles R.face) ≤
         Fintype.card α + 2 * Nat.card (Quotient R.components) := by
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.Ribbon, OAI.KaplanskyCounterexample.Planar.Cycles