card_inter_lt_of_cliqueFree — Mathlib

English

Under a concatenated hypothesis, there exists a five-wheel-like structure with k+1.

Русский

При совокупности условий существует структура, подобная FiveWheelLike, с параметрами k+1.

LaTeX

$$$$ \\exists a,b:\\; G.IsFiveWheelLike r (k+1) v w_1 w_2 (insert a s) (insert b t). $$$$

Lean4

theorem card_inter_lt_of_cliqueFree (h : G.CliqueFree (r + 2)) : k < r :=
  by
  contrapose! h
  have hs := eq_of_subset_of_card_le inter_subset_left (hw.card_inter ▸ hw.card_left ▸ h)
  have := eq_of_subset_of_card_le inter_subset_right (hw.card_inter ▸ hw.card_right ▸ h)
  exact
    (hw.isNClique_fst_left.insert_insert (hs ▸ this.symm ▸ hw.isNClique_snd_right) hw.snd_notMem_left
        hw.isPathGraph3Compl.adj).not_cliqueFree

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