Icc — Mathlib

English

In a locally finite order, the finset Icc(a,b) consists of all elements x with a ≤ x ≤ b.

Русский

В локально конечном порядке финсет Icc(a,b) состоит из всех элементов x, удовлетворяющих a ≤ x ≤ b.

LaTeX

$$$Icc(a,b) = \{ x \in \alpha \mid a \le x \le b \}$$$

Lean4

/-- The finset $[a, b]$ of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a
finset. -/
def Icc (a b : α) : Finset α :=
  LocallyFiniteOrder.finsetIcc a b

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