cliqueFreeOn_empty — Mathlib

English

For any graph G and n, G is n-clique-free on the empty set if and only if n ≠ 0.

Русский

Для любого графа G и любого n граф G не содержит n‑клик на пустом множестве тогда и только тогда, когда n ≠ 0.

LaTeX

$$For all $G$ and $n$, $G$ is $n$-clique-free on $\emptyset$ iff $n \neq 0$.$$

Lean4

@[simp]
theorem cliqueFreeOn_empty : G.CliqueFreeOn ∅ n ↔ n ≠ 0 := by simp [CliqueFreeOn, Set.subset_empty_iff]

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