refl

Mathlib.Data.QPF.Multivariate.Constructions.Fix

URI: https://scilib.ai/kg/mathlib#MvQPF.wEquiv.refl

English

Every element is W-equivalent to itself. For all α and x ∈ (q.P.W α), WEquiv x x holds.

Русский

Каждый элемент эквивалентен самому себе относительно WEquiv.

LaTeX

$$$\forall {\alpha : TypeVec n} (x : (q.P F).W \alpha), WEquiv x x$$$

Lean4

theorem refl {α : TypeVec n} (x : q.P.W α) : WEquiv x x :=
  abs' x x rfl

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

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

Разделы

Аффилиация

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