lcs_add_le_iff — Mathlib

English

The lcs of a sum index satisfies a transposed inequality with UCS.

Русский

Серия нижней центральной серии при сумме индексов удовлетворяет неравенству, противоположному UCS.

LaTeX

$$$\\operatorname{lcs}(l+k)\\le N_2 \\iff \\operatorname{lcs}(l)\\le N_2.ucs(k).$$$

Lean4

theorem lcs_add_le_iff (l k : ℕ) : N₁.lcs (l + k) ≤ N₂ ↔ N₁.lcs l ≤ N₂.ucs k := by
  induction k generalizing l with
  | zero => simp
  | succ k ih => rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]

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