English
If α is nonempty and s is finite, and the sum of |f(i)| over s is at most n, then there exists β, a tagging sgn:β→SignType and g:β→α with certain zero-avoidance and cardinality constraints, reproducing f on s.
Русский
Если α непусто, s — конечное множество, и сумма |f(i)| по i∈s не превосходит n, существует β, отображение sgn:β→SignType и g:β→α со свойствами нулевого поведения за пределами s и кардинальности равной n, которые восстанавливают f на s.
LaTeX
$$$\exists \beta \; (Fintype \beta) \; (\text{sgn}: \beta \to SignType) \; (g: \beta \to \alpha),\; (\forall b, g b \notin s \to \operatorname{sgn} b = 0) \land (Eq (Fintype.card \beta) n) \land (\forall a \in s, \sum_{b} \text{if } g b = a \text{ then } (\text{sgn} b).cast 0 \text{ else } 0) = f a$$$
Lean4
/-- `SignType` is equivalent to `Fin 3`. -/
def fin3Equiv : SignType ≃* Fin 3
where
toFun
a :=
match a with
| 0 => ⟨0, by simp⟩
| 1 => ⟨1, by simp⟩
| -1 => ⟨2, by simp⟩
invFun
a :=
match a with
| ⟨0, _⟩ => 0
| ⟨1, _⟩ => 1
| ⟨2, _⟩ => -1
left_inv a := by cases a <;> rfl
right_inv
a :=
match a with
| ⟨0, _⟩ => by simp
| ⟨1, _⟩ => by simp
| ⟨2, _⟩ => by simp
map_mul' a b := by cases a <;> cases b <;> rfl
