α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
inst✝ : Fintype α
f : ⊤ ↪g G
⊢ Nonempty (⊤ ↪g G)
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
inst✝ : Fintype α
f : ⊤ ↪g G
⊢ ¬CliqueFree G (Fintype.card α)
rw [not_cliqueFree_iff]
no goals
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
inst✝ : Fintype α
f : ⊤ ↪g G
⊢ Nonempty (⊤ ↪g G)
exact ⟨(Iso.completeGraph (Fintype.equivFin α)).symm.toEmbedding.trans f⟩