Ioi_False

Mathlib.Order.Interval.Set.Basic

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

English

In the same two-element chain, the right-open interval above False contains only True: Ioi(False) = { True }.

Русский

В той же двоичной цепи справа открытый интервал над False содержит только True: Ioi(False) = { True }.

LaTeX

$$$Ioi(False) = \{True\}$$$

Lean4

@[simp]
theorem Ioi_False : Ioi False = { True } := by aesop (add simp [Ioi, lt_iff_le_not_ge])

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

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

Разделы

Аффилиация

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