trivial

Mathlib.Deprecated.Estimator

URI: https://scilib.ai/kg/mathlib#Estimator.trivial

Lean4

/-- A trivial estimator, containing the actual value. -/
abbrev trivial.{u} {α : Type u} (a : α) : Type u :=
  { b : α // b = a }

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

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

Разделы

Аффилиация

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