Theorems · Definition · combinatorics

SimpleGraph.IsPathGraph3Compl.recOn

{α : Type u} →
  {G : SimpleGraph α} →
    {v w₁ w₂ : α} →
      {motive : G.IsPathGraph3Compl v w₁ w₂ → Sort u_1} →
        (t : G.IsPathGraph3Compl v w₁ w₂) →
          ((adj : G.Adj w₁ w₂) → (not_adj_fst : ¬G.Adj v w₁) → (not_adj_snd : ¬G.Adj v w₂) → motive ⋯) → motive t

Defined in: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Cited by: 0 results in Mathlib
Foundations: Depth 4 from the axioms · uses no axioms

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

SimpleGraphstatement and proof · cited by 3,072
SimpleGraph.Adjstatement and proof · cited by 1,346
SimpleGraph.IsPathGraph3Complstatement and proof · cited by 12

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.