agree_trivial

Mathlib.Data.PFunctor.Univariate.M

URI: https://scilib.ai/kg/mathlib#PFunctor.Approx.agree_trivial

English

The base case of agreement between two trivial approximations is always true.

Русский

Базовый случай согласия между двумя тривиальными аппроксимациями всегда верен.

LaTeX

$$@[simp] theorem agree_trivial {x : CofixA F 0} {y : CofixA F 1} : Agree x y := by constructor$$

Lean4

@[simp]
theorem agree_trivial {x : CofixA F 0} {y : CofixA F 1} : Agree x y := by constructor

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

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

Разделы

Аффилиация

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