mem_Ioc_succ'

Mathlib.Order.Interval.Finset.Nat

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

English

The interval Ioc(b, b+1) has a unique element, namely b+1, viewed as a natural with its membership proof.

Русский

У интервала Ioc(b, b+1) имеется единственный элемент, равный b+1, с доказательством принадлежности.

LaTeX

$$$Ioc(b, b+1) = \\{b+1\\}$$$

Lean4

theorem mem_Ioc_succ' (a : Ioc b (b + 1)) : a = ⟨b + 1, mem_Ioc.2 (by omega)⟩ :=
  Subtype.val_inj.1 (mem_Ioc_succ.1 a.2)

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

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

Разделы

Аффилиация

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