toList_injective

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.toList_injective

English

The function RelSeries.toList is injective.

Русский

Функция RelSeries.toList инъективна.

LaTeX

$$∃ x y : RelSeries r, x ≠ y ∧ x.toList ≠ y.toList → true$$

Lean4

theorem toList_injective : Function.Injective (RelSeries.toList (r := r)) := fun _ _ h ↦
  (RelSeries.Equiv).injective <| Subtype.ext h

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

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

Разделы

Аффилиация

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