filter_lt_of_succ_bot — Mathlib

English

If n < m, then filtering Ico(n, m) by x < n+1 yields the singleton [n].

Русский

Если n < m, то отсев Ico(n, m) по x < n+1 даёт единственный элемент [n].

LaTeX

$$$$ n < m \\implies \\{x \\in \\mathbb{N} \\mid n \\le x < m \\land x < n+1\\} = \\{n\\}. $$$$

Lean4

theorem filter_lt_of_succ_bot {n m : ℕ} (hnm : n < m) : ((Ico n m).filter fun x => x < n + 1) = [n] :=
  by
  have r : min m (n + 1) = n + 1 := (@inf_eq_right _ _ m (n + 1)).mpr hnm
  simp [filter_lt n m (n + 1), r]

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