left_notMem_Ioc

Mathlib.Order.Interval.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.left_notMem_Ioc

English

The left endpoint a does not belong to Ioc(a,b).

Русский

Левый предел a не принадлежит Ioc(a,b).

LaTeX

$$$ a \notin Ioc\ a\ b $$$

Lean4

theorem left_notMem_Ioc : a ∉ Ioc a b :=
  Finset.left_notMem_Ioc

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

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

Разделы

Аффилиация

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