ext

Mathlib.Order.Synonym

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

English

If two elements a,b ∈ αᵒᵈ have the same image under ofDual, then a = b.

Русский

Если для элементов a,b ∈ αᵒᵈ их образы под ofDual совпадают, то a = b.

LaTeX

$$$\operatorname{ofDual} a = \operatorname{ofDual} b \Rightarrow a=b$$$

Lean4

@[ext]
theorem ext {a b : αᵒᵈ} (h : ofDual a = ofDual b) : a = b :=
  h

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

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

Разделы

Аффилиация

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