abs' — Mathlib

English

If the underlying representations of x and y have the same absolute value, then x and y are Wequiv.

Русский

Если основания представлений x и y совпадают по модулю abs, то x и y эквивальны по Wequiv.

LaTeX

$$$$\forall {F : Type u \to Type v} [q : QPF F] (x y : (q.P F).W) (h : q.abs x.dest = q.abs y.dest), Wequiv x y.$$$$

Lean4

theorem abs' (x y : q.P.W) (h : QPF.abs x.dest = QPF.abs y.dest) : Wequiv x y :=
  by
  cases x
  cases y
  apply Wequiv.abs
  apply h

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