triangleRemovalBound_pos

Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

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

← MathLib Explorer

English

Explicit bound for triangle removal constant as a function of ε.

Русский

Явное ограничение константы удаления треугольников как функция ε.

LaTeX

$$triangleRemovalBound ε = ...$$

Lean4

theorem triangleRemovalBound_pos (hε : 0 < ε) : 0 < triangleRemovalBound ε :=
  by
  have : 0 < 1 - min 1 ε / 4 := by have := min_le_left 1 ε; linarith
  unfold triangleRemovalBound
  positivity

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

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

Разделы

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

Аффилиация

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