Documentation

FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Clique

source
def SimpleGraph.«termα(_)» :
Lean.ParserDescr

The maximal number of vertices of an independent set in a graph G.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SimpleGraph.indepNum_of_isEmpty {V : Type u_1} {G : SimpleGraph V} [IsEmpty V] :
    G.indepNum = 0
    source
    @[simp]
    theorem SimpleGraph.indepNum_pos {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nonempty V] :
    0 < G.indepNum
    source
    noncomputable def SimpleGraph.ecliqueNum {V : Type} (G : SimpleGraph V) :
    ℕ∞

    Infinite graphs: definitions for clique number so that the clique number of a graph with unbounded clique size is ∞ rather than 0.

    Equations
    Instances For