α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ IsClique G ↑s ∧ Finset.card s = n → IsClique H ↑s ∧ Finset.card s = n
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ IsNClique G n s → IsNClique H n s
simp_rw [isNClique_iff]
no goals
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ IsClique G ↑s ∧ Finset.card s = n → IsClique H ↑s ∧ Finset.card s = n
exact And.imp_left (IsClique.mono h)