ofDual_apply_coe

Mathlib.Order.WithBot

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

English

For a ∈ αᵒᵈ, the equality WithTop.ofDual(a : WithTop αᵒᵈ) = ofDual(a) holds, describing compatibility of ofDual with coe.

Русский

Для a ∈ αᵒᵈ верно, что WithTop.ofDual(a : WithTop αᵒᵈ) = ofDual(a).

LaTeX

$$$\\mathrm{WithTop.ofDual}(a:\\mathrm{WithTop}(\\alpha^{\\mathrm{op}})) = \\mathrm{ofDual}(a)$$$

Lean4

@[simp]
theorem ofDual_apply_coe (a : αᵒᵈ) : WithTop.ofDual (a : WithTop αᵒᵈ) = ofDual a :=
  rfl

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

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

Разделы

Аффилиация

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