uIcc — Mathlib

English

In a lattice, the unordered interval uIcc(a,b) is the closed interval between a ∧ b and a ∨ b.

Русский

В решётке неупорядоченная интервал uIcc(a,b) есть замкнутый интервал между a ∧ b и a ∨ b.

LaTeX

$$$$ \mathrm{uIcc}(a,b) = Icc(a \wedge b, a \vee b). $$$$

Lean4

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

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