Ioo_coe — Mathlib

English

Let α be a preorder. The open interval between a and b in the extended type WithBot α is exactly the image of the open interval (a, b) in α under the canonical embedding α → WithBot α.

Русский

Пусть α — частично упорядоченное множество. Открытый интервал между a и b в расширении WithBot α равен образу интервала (a, b) в α через естественное вложение α → WithBot α.

LaTeX

$$$Ioo\ (a : WithBot \alpha)\ b = (\uparrow) '' (Ioo\ a\ b)$$$

Lean4

theorem Ioo_coe : Ioo (a : WithBot α) b = (↑) '' (Ioo a b) :=
  image_coe_Ioo.symm

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