Iio_nonempty

Mathlib.Order.Interval.Finset.Basic

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

English

In a locally finite preorder, the open lower interval Iio(a) is nonempty exactly when a is not minimal.

Русский

В локально конечно упорядоченном множстве открытый нижний интервал Iio(a) непуст тогда, когда a не минимален.

LaTeX

$$$(Iio(a)).Nonempty \iff \neg IsMin(a)$$$

Lean4

@[simp]
theorem Iio_nonempty : (Iio a).Nonempty ↔ ¬IsMin a := by simp [nonempty_iff_ne_empty]

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

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

Разделы

Аффилиация

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