Iio_True — Mathlib

English

In a two-element order {False < True}, the left-open interval below the maximum element True consists exactly of False: Iio(True) = { False }.

Русский

В двухэлементном порядке {False < True} левый открытый промежуток ниже максимального элемента True состоит ровно из False: Iio(True) = { False }.

LaTeX

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

Lean4

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

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