Euler characteristic of a bipartite ribbon graph

The Euler characteristic agrees with that of any edge-numbered permutation triple. This comparison gives its parity and the connected upper bound.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.eulerChar_toPermutationTriple (Γ : BipartiteRibbonGraph) {n : ℕ} (ν : Γ.E ≃ Fin n) : (Γ.toPermutationTriple ν).eulerChar = Γ.eulerChar

The Euler characteristic of a ribbon graph agrees with that of its permutation triple for any numbering of the edges.

theorem TauCeti.BipartiteRibbonGraph.even_eulerChar (Γ : BipartiteRibbonGraph) : Even Γ.eulerChar

The Euler characteristic of a finite bipartite ribbon graph is even.

theorem TauCeti.BipartiteRibbonGraph.IsConnected.eulerChar_le_two (Γ : BipartiteRibbonGraph) (hΓ : Γ.IsConnected) : Γ.eulerChar ≤ 2

A connected bipartite ribbon graph has Euler characteristic at most two.