Iio_inj — Mathlib

English

In a linear order, the left ray (−∞, a) uniquely determines a; thus, if (−∞, a) = (−∞, b) then a = b (and conversely).

Русский

В линейном порядке луч слева (−∞, a) однозначно задаёт a; следовательно, если (−∞, a) = (−∞, b), то a = b (и наоборот).

LaTeX

$$$ (−\infty, a) = (−\infty, b) \iff a = b $$$

Lean4

theorem Iio_inj : Iio a = Iio b ↔ a = b :=
  Iio_injective.eq_iff

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