nonpos — Mathlib

English

If G is far from triangle-free, then its cliqueFinset 3 is nonempty under assumptions.

Русский

Если граф далёк от треугольников, то cliqueFinset 3 непусто.

LaTeX

$$G.FarFromTriangleFree ε → (G.cliqueFinset 3).Nonempty$$

Lean4

theorem nonpos (h₀ : G.FarFromTriangleFree ε) (h₁ : G.CliqueFree 3) : ε ≤ 0 :=
  by
  have := h₀ (empty_subset _)
  rw [coe_empty, Finset.card_empty, cast_zero, deleteEdges_empty] at this
  exact nonpos_of_mul_nonpos_left (this h₁) (cast_pos.2 <| sq_pos_of_pos Fintype.card_pos)

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