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