V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
⊢ Finset.card s ≤ Fintype.card α
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : IsClique G ↑s
inst✝ : Fintype α
C : Coloring G α
⊢ Finset.card s ≤ Fintype.card α
rw [isClique_iff_induce_eq] at h
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : induce (↑s) G ↪g G
⊢ Finset.card s ≤ Fintype.card α
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
⊢ Finset.card s ≤ Fintype.card α
have f : G.induce ↑s ↪g G := Embedding.comap (Function.Embedding.subtype fun x => x ∈ ↑s) G
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : ⊤ ↪g G
⊢ Finset.card s ≤ Fintype.card α
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : induce (↑s) G ↪g G
⊢ Finset.card s ≤ Fintype.card α
rw [h] at f
case h.e'_3
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : ⊤ ↪g G
⊢ Finset.card s = Fintype.card ↑↑s
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : ⊤ ↪g G
⊢ Finset.card s ≤ Fintype.card α
convert Fintype.card_le_of_injective _ (C.comp f.toHom).injective_of_top_hom using 1
no goals
case h.e'_3
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
s : Finset V
h : induce (↑s) G = ⊤
inst✝ : Fintype α
C : Coloring G α
f : ⊤ ↪g G
⊢ Finset.card s = Fintype.card ↑↑s
simp