length_eq_four — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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