Documentation

ExponentialRamsey.Prereq.Mathlib.Combinatorics.SimpleGraph.Basic

Stuff for combinatorics.simple_graph.basic #

source
instance SimpleGraph.instIsEmptyElemSym2EdgeSetOfSubsingleton_exponentialRamsey {V : Type u_1} {G : SimpleGraph V} [Subsingleton V] :
IsEmpty ↑G.edgeSet
source
def SimpleGraph.topEdgeSetEquiv {V : Type u_1} :
↑⊤.edgeSet ≃ { a : Sym2 V // ¬a.IsDiag }

The edge set of the complete graph on V is in bijection with the off-diagonal elements of sym2 V TODO: maybe this should be an equality of sets? and then turn it into a bijection of types

Equations
Instances For
    source
    theorem SimpleGraph.card_top_edgeSet {V : Type u_1} [DecidableEq V] [Fintype V] :
    Fintype.card ↑⊤.edgeSet = (Fintype.card V).choose 2
    source
    theorem SimpleGraph.edgeSet_eq_empty_iff {V : Type u_1} {G : SimpleGraph V} :
    G.edgeSet = ∅ ↔ G = ⊥
    source
    theorem SimpleGraph.disjoint_left {V : Type u_1} {G H : SimpleGraph V} :
    Disjoint G H ↔ ∀ (x y : V), G.Adj x y → ¬H.Adj x y
    source
    @[simp]
    theorem SimpleGraph.adj_sup_iff {ι : Type u_5} {V : Type u_6} {s : Finset ι} {f : ι → SimpleGraph V} {x y : V} :
    (s.sup f).Adj x y ↔ ∃ i ∈ s, (f i).Adj x y
    source
    theorem SimpleGraph.top_hom_injective {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} (f : ⊤ →g G) :
    Function.Injective ⇑f
    source
    def SimpleGraph.topHomGraphEquiv {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} :
    ⊤ ↪g G ≃ ⊤ →g G

    graph embeddings from a complete graph are in bijection with graph homomorphisms from it

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem SimpleGraph.neighborSet_bot {V : Type u_1} {x : V} :
      ⊥.neighborSet x = ∅
      source
      theorem SimpleGraph.neighborSet_top {V : Type u_1} {x : V} :
      ⊤.neighborSet x = {x}ᶜ
      source
      theorem SimpleGraph.neighborSet_sup {V : Type u_1} {G H : SimpleGraph V} {x : V} :
      (G ⊔ H).neighborSet x = G.neighborSet x ∪ H.neighborSet x
      source
      theorem SimpleGraph.neighborSet_inf {V : Type u_1} {G H : SimpleGraph V} {x : V} :
      (G ⊓ H).neighborSet x = G.neighborSet x ∩ H.neighborSet x
      source
      theorem SimpleGraph.neighborSet_iSup {V : Type u_1} {ι : Type u_5} {s : ι → SimpleGraph V} {x : V} :
      (⨆ (i : ι), s i).neighborSet x = ⋃ (i : ι), (s i).neighborSet x
      source
      theorem SimpleGraph.neighborSet_iInf {V : Type u_1} {ι : Type u_5} [Nonempty ι] {s : ι → SimpleGraph V} {x : V} :
      (⨅ (i : ι), s i).neighborSet x = ⋂ (i : ι), (s i).neighborSet x
      source
      theorem SimpleGraph.neighborSet_disjoint {V : Type u_1} {G H : SimpleGraph V} {x : V} (h : Disjoint G H) :
      Disjoint (G.neighborSet x) (H.neighborSet x)
      source
      instance SimpleGraph.instIsEmptyElemNeighborSetBot_exponentialRamsey {V : Type u_5} {x : V} :
      IsEmpty ↑(⊥.neighborSet x)
      source
      theorem SimpleGraph.neighborFinset_bot {V : Type u_1} {x : V} [Fintype ↑(⊥.neighborSet x)] :
      ⊥.neighborFinset x = ∅
      source
      theorem SimpleGraph.neighborFinset_top {V : Type u_1} [Fintype V] [DecidableEq V] {x : V} :
      ⊤.neighborFinset x = {x}ᶜ
      source
      theorem SimpleGraph.neighborFinset_sup {V : Type u_1} [DecidableEq V] {G H : SimpleGraph V} {x : V} [Fintype ↑((G ⊔ H).neighborSet x)] [Fintype ↑(G.neighborSet x)] [Fintype ↑(H.neighborSet x)] :
      (G ⊔ H).neighborFinset x = G.neighborFinset x ∪ H.neighborFinset x
      source
      theorem SimpleGraph.neighborFinset_inf {V : Type u_1} [DecidableEq V] {G H : SimpleGraph V} {x : V} [Fintype ↑((G ⊓ H).neighborSet x)] [Fintype ↑(G.neighborSet x)] [Fintype ↑(H.neighborSet x)] :
      (G ⊓ H).neighborFinset x = G.neighborFinset x ∩ H.neighborFinset x
      source
      instance SimpleGraph.Finset.decidableRelSup {ι : Type u_5} {V : Type u_6} {s : Finset ι} {f : ι → SimpleGraph V} [(i : ι) → DecidableRel (f i).Adj] :
      DecidableRel (s.sup f).Adj
      Equations
      source
      theorem SimpleGraph.neighborFinset_supr {V : Type u_1} [DecidableEq V] {ι : Type u_5} {s : Finset ι} {f : ι → SimpleGraph V} {x : V} [(i : ι) → Fintype ↑((f i).neighborSet x)] [Fintype ↑((s.sup f).neighborSet x)] :
      (s.sup f).neighborFinset x = s.biUnion fun (i : ι) => (f i).neighborFinset x
      source
      @[simp]
      theorem SimpleGraph.coe_neighborFinset {V : Type u_1} {G : SimpleGraph V} {x : V} [Fintype ↑(G.neighborSet x)] :
      ↑(G.neighborFinset x) = G.neighborSet x
      source
      theorem SimpleGraph.neighborFinset_disjoint {V : Type u_1} {G H : SimpleGraph V} {x : V} [Fintype ↑(G.neighborSet x)] [Fintype ↑(H.neighborSet x)] (h : Disjoint G H) :
      Disjoint (G.neighborFinset x) (H.neighborFinset x)
      source
      theorem SimpleGraph.degree_eq_zero_iff {V : Type u_1} {G : SimpleGraph V} {v : V} [Fintype ↑(G.neighborSet v)] :
      G.degree v = 0 ↔ ∀ (w : V), ¬G.Adj v w