toDual_ofDual

Mathlib.Order.Synonym

URI: https://scilib.ai/kg/mathlib#OrderDual.toDual_ofDual

English

ToDual(ofDual a) = a for all a in αᵒᵈ.

Русский

ToDual(ofDual a) = a для всех a в αᵒᵈ.

LaTeX

$$$ toDual (ofDual a) = a $$$

Lean4

@[simp]
theorem toDual_ofDual (a : αᵒᵈ) : toDual (ofDual a) = a :=
  rfl

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

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

Разделы

Аффилиация

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