cofixA_eq_zero

Mathlib.Data.PFunctor.Univariate.M

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

English

For any nontrivial approximation F, any x,y in CofixA F 0 are equal; the 0-th approximation is a singleton.

Русский

Для любой нетривиальной аппроксимации F любые x,y ∈ CofixA F 0 равны; 0-я аппроксимация едина.

LaTeX

$$$\forall x,y:\, CofixA F 0,\ x = y.$$$

Lean4

theorem cofixA_eq_zero : ∀ x y : CofixA F 0, x = y
  | CofixA.continue, CofixA.continue => rfl

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

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

Разделы

Аффилиация

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