Documentation

Ramsey2lemmas.SimpleGraph

source
@[simp]
theorem SimpleGraph.induce_compl {V✝ : Type u_1} {G : SimpleGraph V✝} (f : Set V✝) :
(induce f G)ᶜ = induce f Gᶜ
source
theorem SimpleGraph.IsIndepSet.subset {V : Type u_1} {t s : Set V} {G : SimpleGraph V} (h : t ⊆ s) :
G.IsIndepSet s → G.IsIndepSet t
source
@[simp]
theorem SimpleGraph.isNIndepSet_one {V : Type u_1} {s : Finset V} {G : SimpleGraph V} :
G.IsNIndepSet 1 s ↔ ∃ (a : V), s = {a}
source
theorem SimpleGraph.Iso.IsClique {V : Type u_1} (G : SimpleGraph V) {W : Type u_2} (G' : SimpleGraph W) {s : Set V} (iso : G ≃g G') :
G.IsClique s ↔ G'.IsClique (⇑iso.toEquiv '' s)
source
theorem SimpleGraph.Iso.IsIndepSet {V : Type u_1} (G : SimpleGraph V) {W : Type u_2} (G' : SimpleGraph W) {s : Set V} (iso : G ≃g G') :
G.IsIndepSet s ↔ G'.IsIndepSet (⇑iso.toEquiv '' s)
source
theorem SimpleGraph.Iso.IsNClique {V : Type u_1} (G : SimpleGraph V) {W : Type u_2} (G' : SimpleGraph W) {n : ℕ} {s : Finset V} (iso : G ≃g G') :
G.IsNClique n s ↔ G'.IsNClique n (Finset.map iso.toEmbedding s)
source
theorem SimpleGraph.Iso.IsNIndepSet {V : Type u_1} (G : SimpleGraph V) {W : Type u_2} (G' : SimpleGraph W) {n : ℕ} {s : Finset V} (iso : G ≃g G') :
G.IsNIndepSet n s ↔ G'.IsNIndepSet n (Finset.map iso.toEmbedding s)
source
theorem SimpleGraph.Iso.cliqueNum {V : Type u_1} (G : SimpleGraph V) {W : Type u_2} (G' : SimpleGraph W) (iso : G ≃g G') :
G.cliqueNum = G'.cliqueNum
source
theorem SimpleGraph.Iso.indepNum {V : Type u_1} (G : SimpleGraph V) {W : Type u_2} (G' : SimpleGraph W) (iso : G ≃g G') :
G.indepNum = G'.indepNum
source
def SimpleGraph.Iso.compl {V : Type u_1} (G : SimpleGraph V) {W : Type u_2} (G' : SimpleGraph W) (iso : G ≃g G') :
Gᶜ ≃g G'ᶜ
Equations
Instances For
    source
    theorem SimpleGraph.fintype_cliqueNum_bddAbove {α : Type u_2} [Fintype α] (G : SimpleGraph α) :
    BddAbove {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}
    source
    theorem SimpleGraph.fintype_indepNum_bddAbove {α : Type u_2} [Fintype α] (G : SimpleGraph α) :
    BddAbove {n : ℕ | ∃ (s : Finset α), G.IsNIndepSet n s}
    source
    @[simp]
    theorem SimpleGraph.cliqueNum_pos {α : Type u_2} [Fintype α] [ne : Nonempty α] (G : SimpleGraph α) :
    1 ≤ G.cliqueNum
    source
    @[simp]
    theorem SimpleGraph.indepNum_pos {α : Type u_2} [Fintype α] [ne : Nonempty α] (G : SimpleGraph α) :
    1 ≤ G.indepNum
    source
    @[simp]
    theorem SimpleGraph.cliqueNum_top {α : Type u_2} [Fintype α] :
    ⊤.cliqueNum = Fintype.card α
    source
    @[simp]
    theorem SimpleGraph.cliqueNum_bot {α : Type u_2} [Fintype α] [Nonempty α] :
    ⊥.cliqueNum = 1
    source
    @[simp]
    theorem SimpleGraph.indepNum_bot {α : Type u_2} [Fintype α] [Nonempty α] :
    ⊥.indepNum = Fintype.card α
    source
    @[simp]
    theorem SimpleGraph.indepNum_top {α : Type u_2} [Fintype α] [Nonempty α] :
    ⊤.indepNum = 1
    source
    theorem SimpleGraph.exists_isNClique_of_le_cliqueNum {α : Type u_2} [Fintype α] {G : SimpleGraph α} {n : ℕ} (h : n ≤ G.cliqueNum) :
    ∃ (S : Finset α), G.IsNClique n S
    source
    theorem SimpleGraph.exists_isNIndset_of_le_indepNum {α : Type u_2} [Fintype α] {G : SimpleGraph α} {n : ℕ} (h : n ≤ G.indepNum) :
    ∃ (S : Finset α), G.IsNIndepSet n S
    source
    theorem SimpleGraph.cliqueNum_lt_iff_cliqueFree {α : Type u_2} [Fintype α] {x : ℕ} (G : SimpleGraph α) :
    G.cliqueNum < x ↔ G.CliqueFree x
    source
    theorem SimpleGraph.Embedding.indepNum_mono {α β : Type} [Fintype α] {G : SimpleGraph α} {G' : SimpleGraph β} (h : G' ↪g G) :
    G'.indepNum ≤ G.indepNum
    source
    theorem SimpleGraph.Embedding.cliqueNum_mono {α β : Type} [Fintype α] {G : SimpleGraph α} {G' : SimpleGraph β} (h : G' ↪g G) :
    G'.cliqueNum ≤ G.cliqueNum