Finite multigraphs with unordered endpoints

Definition

LeanFormalizations_Combinatorics_CombinatorialMap_PlanarEdgeBound

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatorics

This records a finite vertex type, a finite edge type, and an unordered pair of endpoints for each edge. It also supplies finite types for individual face and edge cycles in a combinatorial map.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_LeanFormalizations_Combinatorics_CombinatorialMap_Basic
import Mathlib
import Mathlib.Data.Sym.Sym2

set_option autoImplicit true

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


open scoped BigOperators

namespace CombinatorialMap

variable {D : Type*} {M : CombinatorialMap D}

noncomputable instance instFintypeFaceSameCycle [Fintype D] {w : D} :
    Fintype {u | M.facePerm.SameCycle w u} :=
  Fintype.ofFinite _


noncomputable instance instFintypeEdgeSameCycle [Fintype D] {w : D} :
    Fintype {u | M.edgePerm.SameCycle w u} :=
  Fintype.ofFinite _


end CombinatorialMap


structure AbstractPlanarizedMultigraph where
  Vertex : Type
  Edge : Type
  vertexFintype : Fintype Vertex
  edgeFintype : Fintype Edge
  edgeVerts : Edge → Sym2 Vertex

attribute [instance] AbstractPlanarizedMultigraph.vertexFintype
attribute [instance] AbstractPlanarizedMultigraph.edgeFintype

View graph