of_succ — Mathlib

English

If a set s is $(n+1)$-clique-free, and a ∈ s, then the restriction $s∩N(a)$ is $n$-clique-free.

Русский

Если множество s не содержит клику размера $(n+1)$ и $a∈s$, то ограничение $s∩N(a)$ не содержит клику размера $n$.

LaTeX

$$If $s$ is $(n+1)$-clique-free and $a∈s$, then $s∩N(a)$ is $n$-clique-free.$$

Lean4

theorem of_succ (hs : G.CliqueFreeOn s (n + 1)) (ha : a ∈ s) : G.CliqueFreeOn (s ∩ G.neighborSet a) n := by
  classical
  refine fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)
  push_cast
  exact Set.insert_subset_iff.2 ⟨ha, hts.trans Set.inter_subset_left⟩

Похожие утверждения