Iio_False — Mathlib

English

Let a be the least element of a preorder. Then there are no elements strictly smaller than a, hence the left-open interval below a is empty. In particular, Iio(False) = ∅.

Русский

Пусть a является наименьшим элементом порядком. Тогда не существует элементов строго меньше a, следовательно, левый открытый интервал ниже a пуст. В частном случае Iio(False) = ∅.

LaTeX

$$$Iio(False) = \emptyset$$$

Lean4

theorem Iio_False : Iio False = ∅ := by aesop

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