coe_lt_top

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.coe_lt_top

English

For any a ∈ α with LT structure, (a : WithTop α) < ⊤ holds.

Русский

Для любого a ∈ α при наличии LT, (a : WithTop α) < ⊤ выполняется.

LaTeX

$$$\forall a : α, (a : \mathrm{WithTop}(\alpha)) < \top$$$

Lean4

@[simp]
theorem coe_lt_top (a : α) : (a : WithTop α) < ⊤ := by simp [lt_def]

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

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

Разделы

Аффилиация

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