FiveWheelLikeFree — Mathlib

English

There is no IsFiveWheelLike structure in G with given parameters; i.e., for all v,w1,w2,s,t, the proposition is false.

Русский

В графе G с заданными параметрами не существует структуры FiveWheelLike; то есть для любых v,w1,w2,s,t истинность не выполняется.

LaTeX

$$$$ \\forall v,w_1,w_2,s,t:\\; \\neg G.IsFiveWheelLike r k v w_1 w_2 s t. $$$$

Lean4

/-- `G.FiveWheelLikeFree r k` means there is no `IsFiveWheelLike r k` structure in `G`. -/
def FiveWheelLikeFree (G : SimpleGraph α) (r k : ℕ) : Prop :=
  ∀ {v w₁ w₂ s t}, ¬G.IsFiveWheelLike r k v w₁ w₂ s t

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