disjoint_Ioi_Iio — Mathlib

English

For any a, the sets Ioi a and Iio a are disjoint; i.e., there is no element strictly greater than a and strictly less than a at the same time.

Русский

Для любого a множества Ioi a и Iio a не пересекаются; элемент не может быть одновременно больше и меньше a.

LaTeX

$$$\operatorname{Disjoint}(\mathrm{Ioi}(a), \mathrm{Iio}(a)).$$$

Lean4

theorem disjoint_Ioi_Iio (a : α) : Disjoint (Ioi a) (Iio a) :=
  disjoint_left.2 fun _ hab hba => (mem_Ioi.1 hab).not_gt <| mem_Iio.1 hba

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