α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
h : 2 ≤ n
t : Finset α
ht : IsNClique ⊥ n t
⊢ False
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
h : 2 ≤ n
⊢ CliqueFree ⊥ n
intro t ht
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
h : 2 ≤ n
t : Finset α
ht : IsNClique ⊥ n t
this : 2 ≤ 1
⊢ False
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
h : 2 ≤ n
t : Finset α
ht : IsNClique ⊥ n t
⊢ False
have := le_trans h (isNClique_bot_iff.1 ht).1
no goals
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
h : 2 ≤ n
t : Finset α
ht : IsNClique ⊥ n t
this : 2 ≤ 1
⊢ False
simp only at this