length_eq_two — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem length_eq_two {v : FreeMonoid α} : v.length = 2 ↔ ∃ c d, v = FreeMonoid.of c * FreeMonoid.of d :=
  List.length_eq_two

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