uIoo — Mathlib

English

uIoo(a, b) is the set of elements strictly between a and b, irrespective of their order.

Русский

uIoo(a, b) — множество элементов строго между a и b независимо от их порядка.

LaTeX

$$$ uIoo(a,b) = Ioo(\min(a,b), \max(a,b)) $$$

Lean4

/-- `uIoo a b` is the set of elements lying between `a` and `b`, with `a` and `b` not included.
Note that we define it more generally in a lattice as `Set.Ioo (a ⊓ b) (a ⊔ b)`. In a product type,
`uIoo` corresponds to the bounding box of the two elements. -/
def uIoo (a b : α) : Set α :=
  Ioo (a ⊓ b) (a ⊔ b)

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