toDualProd_injective

Mathlib.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#NonemptyInterval.toDualProd_injective

English

The map s ↦ s.toDualProd is injective; if s.toDualProd = t.toDualProd, then s = t.

Русский

Отображение s ↦ s.toDualProd инъективно: если s.toDualProd = t.toDualProd, то s = t.

LaTeX

$$$\\forall s,t \in \text{NonemptyInterval } \alpha,\; s.toDualProd = t.toDualProd \Rightarrow s = t.$$$

Lean4

theorem toDualProd_injective : Injective (toDualProd : NonemptyInterval α → αᵒᵈ × α) :=
  toProd_injective

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

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

Разделы

Аффилиация

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