Ioo_eq_zero — Mathlib

English

Let a and b be elements of a locally finite preorder. If a is not less than b, then the open interval between a and b is empty.

Русский

Пусть a и b — элементы локально конечного предварительного порядка. Если a не меньше b, то открытый интервал (a, b) пуст.

LaTeX

$$$ Ioo\ a\ b = 0 $$$

Lean4

@[simp]
theorem Ioo_eq_zero (h : ¬a < b) : Ioo a b = 0 :=
  eq_zero_iff_forall_notMem.2 fun _x hx => h ((mem_Ioo.1 hx).1.trans (mem_Ioo.1 hx).2)

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