instUniqueSigmaNatRelations

Mathlib.ModelTheory.Order

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.order.instUniqueSigmaNatRelations

English

There exists a unique element of the form (n, R) in the codomain, namely (2, le).

Русский

Существует единственный элемент вида (n, R) в тогеении, а именно (2, le).

LaTeX

$$$ \\text{Unique }(\\Sigma n, Language.order.Relations n) $$$

Lean4

instance : Unique (Σ n, Language.order.Relations n) :=
  ⟨⟨⟨2, .le⟩⟩, fun ⟨n, R⟩ =>
    match n, R with
    | 2, .le => rfl⟩

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

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

Разделы

Аффилиация

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