length_eq_three — Mathlib

English

For any v, length(v) = 3 if and only if there exist a, b, c in α such that v = of a * of b * of c.

Русский

Для любого v: length(v) = 3 тогда и только тогда, когда существуют a, b, c ∈ α такие, что v = of a * of b * of c.

LaTeX

$$$\\\\operatorname{length}(v) = 3 \\\\iff \\\\exists a \\\\exists b \\\\exists c, \\\\ v = \\\\operatorname{of} a * \\\\operatorname{of} b * \\\\operatorname{of} c$$$

Lean4

@[to_additive]
theorem length_eq_three {v : FreeMonoid α} : v.length = 3 ↔ ∃ (a b c : α), v = of a * of b * of c :=
  List.length_eq_three

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