Icc_bot_coe — Mathlib

English

Let α be a locally finite ordered type with a bottom element. In the extension WithBot α, the closed interval from the bottom element to b is exactly the bottom element together with all elements of α that are ≤ b. Symbolically, Icc(⊥, b) = insertNone(Iic b).

Русский

Пусть α – локально конечное упорядоченное множество с нижней границей. В расширении WithBot α замкнутый интервал [⊥, b] состоит из нижнего элемента и всех элементов α, не превосходящих b. То есть Icc(⊥, b) = insertNone(Iic b).

LaTeX

$$$$ \\mathrm{Icc}(\\perp, b) = \\mathrm{insertNone}\\bigl( \\mathrm{Iic}\\, b \\bigr). $$$$

Lean4

theorem Icc_bot_coe : Icc (⊥ : WithBot α) b = insertNone (Iic b) :=
  rfl

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