insert_erase — Mathlib

English

If inserting a vertex a into s while maintaining adjacencies to all in s preserves NClique, then the enlarged set is an NClique with increased n by 1.

Русский

Если при добавлении вершины a к множеству s сохраняется свойство NClique, то новое множество является NClique с увеличенным на единицу размером n.

LaTeX

$$$$ G.IsNClique\\ n\\ s \\rightarrow (\\forall b \\in s, G.Adj a b) \\rightarrow G.IsNClique\\ (n+1)\\ (insert\\ a\\ s) $$$$

Lean4

protected theorem insert_erase (hs : G.IsNClique n s) (ha : ∀ w ∈ s \ { b }, G.Adj a w) (hb : b ∈ s) :
    G.IsNClique n (insert a (erase s b)) := by
  cases n with
  | zero => exact False.elim <| notMem_empty _ (isNClique_zero.1 hs ▸ hb)
  | succ _ => exact (hs.erase_of_mem hb).insert fun w h ↦ by aesop

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