Ioi_disjoint_Iio_iff — Mathlib

English

Ioi(a) and Iio(b) are disjoint iff not a < b, under dense order.

Русский

При плотном порядке Ioi(a) и Iio(b) непересекаются тогда и только тогда, когда не выполняется a < b.

LaTeX

$$$$ Disjoint (Ioi\,a) (Iio\,b) \iff \neg(a < b) \quad [\text{DenselyOrdered } \alpha]. $$$$

Lean4

@[simp]
theorem Ioi_disjoint_Iio_iff [DenselyOrdered α] : Disjoint (Ioi a) (Iio b) ↔ ¬a < b :=
  ⟨fun h hab ↦ (exists_between hab).elim fun _ hc ↦ h.notMem_of_mem_left hc.left hc.right, Ioi_disjoint_Iio_of_not_lt⟩

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