mem_range

Mathlib.Data.Finset.Range

URI: https://scilib.ai/kg/mathlib#Finset.mem_range

English

For natural numbers n and m, m belongs to range(n) if and only if m < n.

Русский

Для натуральных чисел n и m выполняется: m ∈ range(n) тогда и только тогда, когда m < n.

LaTeX

$$$$ m \in \operatorname{range}(n) \;\iff\; m < n. $$$$

Lean4

@[simp, grind =]
theorem mem_range : m ∈ range n ↔ m < n :=
  Multiset.mem_range

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru