mem_range_succ_iff

Mathlib.Data.Finset.Range

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

English

An element a belongs to range(b+1) if and only if a ≤ b.

Русский

Элемент a принадлежит диапазону b+1 тогда и только тогда, когда a ≤ b.

LaTeX

$$$$ a \in \operatorname{range}(b+1) \iff a \le b. $$$$

Lean4

theorem mem_range_succ_iff {a b : ℕ} : a ∈ range b.succ ↔ a ≤ b := by grind

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

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

Разделы

Аффилиация

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