notMem_Ico_of_lt

Mathlib.Order.Interval.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.notMem_Ico_of_lt

English

Let α be a type with a preorder. For all a,b,c ∈ α, if c < a then c ∉ Ico(a,b).

Русский

Пусть α имеет предикат порядка. Пусть a,b,c ∈ α. Если c < a, то c не принадлежит Ico(a,b).

LaTeX

$$$ \forall \alpha\,[Preorder\,\alpha],\ \forall a,b,c\in\alpha,\ c

Lean4

theorem notMem_Ico_of_lt (ha : c < a) : c ∉ Ico a b := fun h => ha.not_ge h.1

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

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

Разделы

Аффилиация

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