mem_Ioc_succ

Mathlib.Order.Interval.Finset.Nat

URI: https://scilib.ai/kg/mathlib#Nat.mem_Ioc_succ

English

For all natural numbers a and b, an element a belongs to Ioc(b, b+1) if and only if a = b+1.

Русский

Для любых натуральных a и b элемент a принадлежит Ioc(b, b+1) тогда и только тогда, когда a = b+1.

LaTeX

$$$a \\in Ioc(b, b+1) \\iff a = b+1$$$

Lean4

theorem mem_Ioc_succ : a ∈ Ioc b (b + 1) ↔ a = b + 1 := by simp

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

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

Разделы

Аффилиация

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