delta — Mathlib

English

A fixed internal parameter used in balancing; delta is defined as 3.

Русский

Фиксированный внутренний параметр, используемый в балансировке; delta определяется как 3.

LaTeX

$$$\delta := 3$$$

Lean4

/-- **Internal use only**

The maximal relative difference between the sizes of
two trees, it corresponds with the `w` in Adams' paper.

According to the Haskell comment, only `(delta, ratio)` settings
of `(3, 2)` and `(4, 2)` will work, and the proofs in
`Ordset.lean` assume `delta := 3` and `ratio := 2`. -/
@[inline]
def delta :=
  3

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