default_eq

Mathlib.Logic.Unique

URI: https://scilib.ai/kg/mathlib#Unique.default_eq

English

In a type with a unique element, the default equals every element.

Русский

В типе с уникальностью значение по умолчанию равно любому элементу.

LaTeX

$$$\mathrm{default} = a$$$

Lean4

theorem default_eq (a : α) : default = a :=
  (uniq _ a).symm

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

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

Разделы

Аффилиация

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