English
If two elements x and y of the W-type have the same absolute value at their destinations, then x and y are W-equivalent: WEquiv x y whenever abs(q.P.wDest' x) = abs(q.P.wDest' y).
Русский
Если у двух элементов x и y типа W одинаковое абсолютное значение на их местах назначения, то x и y эквивалентны по W: WEquiv x y при равенствеabs(q.P.wDest' x) = abs(q.P.wDest' y).
LaTeX
$$$\forall {\alpha : TypeVec n} \forall x y : q.P.W \alpha, \; MvQPF.abs (q.P.wDest' x) = MvQPF.abs (q.P.wDest' y) \Rightarrow WEquiv x y$$$
Lean4
theorem abs' {α : TypeVec n} (x y : q.P.W α) (h : MvQPF.abs (q.P.wDest' x) = MvQPF.abs (q.P.wDest' y)) : WEquiv x y :=
by
revert h
apply q.P.w_cases _ x
intro a₀ f'₀ f₀
apply q.P.w_cases _ y
intro a₁ f'₁ f₁
apply WEquiv.abs
