triangleRemovalBound_nonpos

Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

URI: https://scilib.ai/kg/mathlib#SimpleGraph.triangleRemovalBound_nonpos

← MathLib Explorer

English

If ε ≤ 0, then triangleRemovalBound ε ≤ 0.

Русский

Если ε ≤ 0, то triangleRemovalBound ε ≤ 0.

LaTeX

$$triangleRemovalBound ε ≤ 0$$

Lean4

theorem triangleRemovalBound_nonpos (hε : ε ≤ 0) : triangleRemovalBound ε ≤ 0 := by
  rw [triangleRemovalBound, ceil_eq_zero.2 (div_nonpos_of_nonneg_of_nonpos _ hε)] <;> simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru