nonempty_Ioc

Mathlib.Order.Interval.Finset.Basic

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

English

For LocallyFiniteOrder α, Ico a b is nonempty iff a < b.

Русский

Для локально конечного порядка α Ico a b непусто тогда, когда a < b.

LaTeX

$$$$ (Ico\\ a\\ b).Nonempty \\iff a < b. $$$$

Lean4

@[simp]
theorem nonempty_Ioc : (Ioc a b).Nonempty ↔ a < b := by rw [← coe_nonempty, coe_Ioc, Set.nonempty_Ioc]

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

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

Разделы

Аффилиация

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