bot_eq_coe

Mathlib.Order.WithBot

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

English

If α has a bottom, then ⊥ in WithTop α equals a if and only if ⊥ equals a in α.

Русский

Если в α есть нижний элемент, то ⊥ в WithTop(α) равен элементу a тогда и только тогда, когда ⊥ в α равен a.

LaTeX

$$$\bot = a \iff \bot = a$$$

Lean4

@[simp, norm_cast]
theorem bot_eq_coe [Bot α] {a : α} : (⊥ : WithTop α) = a ↔ ⊥ = a :=
  coe_eq_coe

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

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

Разделы

Аффилиация

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