instWellFoundedGTUnit

Mathlib.Deprecated.Estimator

URI: https://scilib.ai/kg/mathlib#instWellFoundedGTUnit

English

There exists a well-founded greater-than relation on the one-element type Unit.

Русский

Существует хорошо основанное отношение GT на одноэлементном типе Unit.

LaTeX

$$WellFoundedGT Unit$$

Lean4

instance : WellFoundedGT Unit where wf := ⟨fun .unit => ⟨Unit.unit, nofun⟩⟩

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

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

Разделы

Аффилиация

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