witness — Mathlib

English

There exists a finite set of group elements witnessing that a given equidecomposition f is valid.

Русский

Существует конечное множество элементов группы, служащее свидетелем действительности данной эквидекомпозиции f.

LaTeX

$$$\text{witness}(f) \;:\; \text{Finset}(G) \text{ witness } f \text{ is a finite witness set for } f.$$$

Lean4

/-- A finite set of group elements witnessing that `f` is an equidecomposition. -/
noncomputable def witness (f : Equidecomp X G) : Finset G :=
  f.isDecompOn'.choose

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