triangleRemovalBound_le — Mathlib

English

For ε ≤ 1, triangleRemovalBound ε is bounded above by a certain expression involving ε, bound, and ⌈4/ε⌉.

Русский

Для ε ≤ 1 triangleRemovalBoundε ограничен сверху выражением, зависящим от ε и других параметров.

LaTeX

$$triangleRemovalBound ε ≤ (1 - ε/4) * (ε/(16 * bound(ε/8) ⌈4/ε⌉₊))^3$$

Lean4

theorem triangleRemovalBound_le (hε₁ : ε ≤ 1) :
    triangleRemovalBound ε ≤ (1 - ε / 4) * (ε / (16 * bound (ε / 8) ⌈4 / ε⌉₊)) ^ 3 := by
  simp [triangleRemovalBound, hε₁]

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