symm — Mathlib

English

Wequiv is symmetric: if x is Wequiv to y, then y is Wequiv to x.

Русский

Wequiv симметрично: если x эквивалентно y, то y эквивалентно x.

LaTeX

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

Lean4

theorem symm (x y : q.P.W) : Wequiv x y → Wequiv y x := by
  intro h
  induction h with
  | ind a f f' _ ih => exact Wequiv.ind _ _ _ ih
  | abs a f a' f' h => exact Wequiv.abs _ _ _ _ h.symm
  | trans x y z _ _ ih₁ ih₂ => exact QPF.Wequiv.trans _ _ _ ih₂ ih₁

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