lt_replicate_succ — Mathlib

English

For m ∈ Multiset α, x ∈ α, n ∈ ℕ, m < replicate(n+1) x iff m ≤ replicate n x.

Русский

Для m ∈ Multiset α, x ∈ α, n ∈ ℕ, m < replicate(n+1) x эквивалентно m ≤ replicate n x.

LaTeX

$$$ m \\lt \\operatorname{replicate}(n+1,x) \\iff m \\le \\operatorname{replicate}(n,x)$$$

Lean4

theorem lt_replicate_succ {m : Multiset α} {x : α} {n : ℕ} : m < replicate (n + 1) x ↔ m ≤ replicate n x :=
  by
  rw [lt_iff_cons_le]
  constructor
  · rintro ⟨x', hx'⟩
    have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))
    rwa [this, replicate_succ, cons_le_cons_iff] at hx'
  · intro h
    rw [replicate_succ]
    exact ⟨x, cons_le_cons _ h⟩

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