Iio_bot — Mathlib

English

In any ordered set with a least element, there are no elements strictly below the least element; thus the open lower interval below the bottom is empty.

Русский

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

LaTeX

$$$Iio(\bot) = \emptyset$$$

Lean4

@[simp]
nonrec theorem Iio_bot [OrderBot α] : Iio (⊥ : α) = ⊥ :=
  SetLike.coe_injective Iio_bot

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