size

Mathlib.Combinatorics.Optimization.ValuedCSP

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

English

The size of a fractional operation is the number of outputs it contains, i.e., the cardinality of the multiset.

Русский

Размер фракционной операции равен числу выходов в мультисете.

LaTeX

$$$\\text{size}(\\omega) = |\\omega|$$$

Lean4

/-- Arity of the "output" of the fractional operation. -/
@[simp]
def size (ω : FractionalOperation D m) : ℕ :=
  ω.card

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

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

Разделы

Аффилиация

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