Theorems · Definition · combinatorics

SimpleGraph.IsFiveWheelLike.recOn

{α : Type u_1} →
  [inst : DecidableEq α] →
    {G : SimpleGraph α} →
      {r k : ℕ} →
        {v w₁ w₂ : α} →
          {s t : Finset α} →
            {motive : G.IsFiveWheelLike r k v w₁ w₂ s t → Sort u} →
              (t_1 : G.IsFiveWheelLike r k v w₁ w₂ s t) →
                ((isPathGraph3Compl : G.IsPathGraph3Compl v w₁ w₂) →
                    (notMem_left : v ∉ s) →
                      (notMem_right : v ∉ t) →
                        (fst_notMem : w₁ ∉ s) →
                          (snd_notMem : w₂ ∉ t) →
                            (isNClique_left : G.IsNClique (r + 1) (insert v s)) →
                              (isNClique_fst_left : G.IsNClique (r + 1) (insert w₁ s)) →
                                (isNClique_right : G.IsNClique (r + 1) (insert v t)) →
                                  (isNClique_snd_right : G.IsNClique (r + 1) (insert w₂ t)) →
                                    (card_inter : (s ∩ t).card = k) → motive ⋯) →
                  motive t_1

Defined in

Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Cited by

0 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq