uIcc — Mathlib

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)

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