Iic — Mathlib

English

The finset of all elements x in the ambient order with x ≤ b (i.e. the interval (-∞, b] represented as a finset).

Русский

Финсет всех элементов x в порядке ≤ такие, что x ≤ b (то есть интервал (-∞, b] в виде финсета).

LaTeX

$$$Iic(b) = \{ x \in \alpha \mid x \le b \}$$$

Lean4

/-- The finset $(-∞, b]$ of elements `x` such that `x ≤ b`. Basically `Set.Iic b` as a finset. -/
def Iic (b : α) : Finset α :=
  LocallyFiniteOrderBot.finsetIic b

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