mem_range_iff — Mathlib

English

For all m,n,r ∈ ℤ, r belongs to range(m,n) if and only if m ≤ r and r < n.

Русский

Для всех m,n,r ∈ ℤ справедливо: r ∈ range(m,n) тогда и только тогда, когда m ≤ r и r < n.

LaTeX

$$$r \in \mathrm{range}(m,n) \iff m \le r \land r < n$$$

Lean4

theorem mem_range_iff {m n r : ℤ} : r ∈ range m n ↔ m ≤ r ∧ r < n :=
  by
  simp only [range, List.mem_map, List.mem_range, lt_toNat, lt_sub_iff_add_lt, add_comm]
  exact
    ⟨fun ⟨a, ha⟩ => ha.2 ▸ ⟨le_add_of_nonneg_right (Int.natCast_nonneg _), ha.1⟩, fun h =>
      ⟨toNat (r - m), by simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2]⟩⟩

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