Ioi_True

Mathlib.Order.Interval.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.Ioi_True

English

In a finite two-element order, there is nothing greater than True, hence Ioi(True) = ∅.

Русский

В двух элементарном порядке сверху True ничего нет, следовательно Ioi(True) = ∅.

LaTeX

$$$Ioi(True) = \emptyset$$$

Lean4

theorem Ioi_True : Ioi True = ∅ := by aesop

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

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

Разделы

Аффилиация

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