strictMono_semilength — Mathlib

English

The semilength increases strictly with respect to the DyckWord order: if p < q then semilength(p) < semilength(q).

Русский

Семилength строго возрастает: если p < q, то semilength(p) < semilength(q).

LaTeX

$$$ p < q \Rightarrow \operatorname{semilength}(p) < \operatorname{semilength}(q) $$$

Lean4

theorem strictMono_semilength : StrictMono semilength := fun p q pq ↦
  by
  obtain ⟨plq, pnq⟩ := lt_iff_le_and_ne.mp pq
  apply lt_of_le_of_ne (monotone_semilength plq)
  contrapose! pnq
  replace pnq := congr(2 * $(pnq))
  simp_rw [two_mul_semilength_eq_length] at pnq
  exact DyckWord.ext ((infix_of_le plq).eq_of_length pnq)

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