le_chainHeight_add_nat_iff — Mathlib

English

For natural numbers n and m, the inequality ↑n ≤ s.chainHeight + m holds if and only if there exists a chain l in s.subchain with n ≤ length(l) + m.

Русский

Для натуральных чисел n и m верно: ↑n ≤ s.chainHeight + m тогда существует цепь l ∈ s.subchain с n ≤ length(l) + m.

LaTeX

$$$ \\uparrow n \\le s.chainHeight + m \\iff \\exists l \\in s.subchain, \\ n \\le \\mathrm{length}(l) + m $$$

Lean4

theorem le_chainHeight_add_nat_iff {n m : ℕ} : ↑n ≤ s.chainHeight + m ↔ ∃ l ∈ s.subchain, n ≤ length l + m := by
  simp_rw [← tsub_le_iff_right, ← ENat.coe_sub, (le_chainHeight_TFAE s (n - m)).out 0 2]

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