IndepSetFreeOn — Mathlib

English

G has no n-independent sets contained in a prescribed subset s.

Русский

У графа G нет n-независимых множеств, которые содержатся в заданном подмножестве s.

LaTeX

$$$\\mathrm{IndepSetFreeOn}(G,s,n) \\;:=\\; \\forall t,\\; \\uparrow t \\subseteq s \\;\\rightarrow\\; \\neg G.IsNIndepSet_n(t)$$$

Lean4

/-- `G.IndepSetFreeOn s n` means that `G` has no `n`-independent sets contained in `s`. -/
def IndepSetFreeOn (G : SimpleGraph α) (s : Set α) (n : ℕ) : Prop :=
  ∀ ⦃t⦄, ↑t ⊆ s → ¬G.IsNIndepSet n t

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