coe_pure

Mathlib.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#NonemptyInterval.coe_pure

English

The set underlying a pure element a is exactly the singleton {a}.

Русский

Множество, соответствующее чистому интервалу (pure a), равно одиночному множеству {a}.

LaTeX

$$$ (pure\ a : NonemptyInterval α) \, : \, Set α = \{a\} $$$

Lean4

@[simp, norm_cast]
theorem coe_pure (a : α) : (pure a : Set α) = { a } :=
  Icc_self _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru