Iio_eq_empty — Mathlib

English

In any preorder with a locally finite order that has a bottom, the set of elements strictly less than a is empty exactly when a is a minimal element.

Русский

В любом частично упорядоченном множестве с локально конечной структурой и существованием низа множество элементов, меньших a, пусто тогда и только тогда a является минимальным элементом.

LaTeX

$$$(Iio(a) = \emptyset) \iff IsMin(a)$$$

Lean4

@[simp]
theorem Iio_eq_empty : Iio a = ∅ ↔ IsMin a :=
  Ioi_eq_empty (α := αᵒᵈ)

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