symm — Mathlib

English

If x is W-equivalent to y, then y is W-equivalent to x.

Русский

Если x эквивалентен y по WEquiv, то y эквивалентен x.

LaTeX

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

Lean4

theorem symm {α : TypeVec n} (x y : q.P.W α) : WEquiv x y → WEquiv y x := by intro h;
  induction h with
  | ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm
  | trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁

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