length_pos — Mathlib

English

The length of any element of FreeMagma is positive.

Русский

Длина любого элемента FreeMagma положительна.

LaTeX

$$$0 < \operatorname{length}(x)$$$

Lean4

/-- The length of an element of a free magma is positive. -/
@[to_additive /-- The length of an element of a free additive magma is positive. -/
    ]
theorem length_pos {α : Type u} (x : FreeMagma α) : 0 < x.length :=
  match x with
  | FreeMagma.of _ => Nat.succ_pos 0
  | mul y z => Nat.add_pos_left (length_pos y) z.length

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