uIoc — Mathlib

English

The open-closed unordered interval uIoc(a,b) is defined as the ordinary open-closed interval with the smaller endpoint as the left bound and the larger as the right bound.

Русский

Неупорядоченный открыто-закрытый интервал uIoc(a,b) определяется как обычный открыто-закрытый интервал с меньшей границей слева и большей — справа.

LaTeX

$$$ \\mathrm{uIoc}(a,b) := Ioc(\\min(a,b), \\max(a,b)) $$$

Lean4

/-- The open-closed uIcc with unordered bounds. -/
def uIoc : α → α → Set α := fun a b =>
  Ioc (min a b)
    (max a b)
      -- Below is a capital iota

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