size

Mathlib.Data.Ordmap.Ordnode

URI: https://scilib.ai/kg/mathlib#Ordnode.size

English

O(1) size accessor for an ordered node: size(nil) = 0 and size(node sz l x r) = sz.

Русский

O(1) доступ к размеру упорядоченного узла: size(nil) = 0 и size(node sz l x r) = sz.

LaTeX

$$$\text{size}(\text{nil}) = 0, \quad \text{size}(\text{node}\ sz\ l\ x\ r) = sz$$$

Lean4

/-- O(1). Get the size of the set.

`size {2, 1, 1, 4} = 3` -/
@[inline]
def size : Ordnode α → ℕ
  | nil => 0
  | node sz _ _ _ => sz

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

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

Разделы

Аффилиация

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