English
An element x belongs to uIcc a b iff it lies between a ∧ b and a ∨ b.
Русский
Элемент x принадлежит uIcc a b тогда и только тогда, когда a ∧ b ≤ x ≤ a ∨ b.
LaTeX
$$x ∈ uIcc a b ↔ a ⊓ b ≤ x ∧ x ≤ a ⊔ b$$
Lean4
/-- `Finset.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 `Finset.Icc (a ⊓ b) (a ⊔ b)`. In a
product type, `Finset.uIcc` corresponds to the bounding box of the two elements. -/
def uIcc (a b : α) : Finset α :=
Icc (a ⊓ b) (a ⊔ b)