flip_flip — Mathlib

English

The flip operation on bilinear continuous linear maps is an involution: applying it twice returns the original map.

Русский

Операция flip над билинейными непрерывными отображениями является инволюцией: применение дважды возвращает исходное отображение.

LaTeX

$$$$ (f^{\mathrm{flip}})^{\mathrm{flip}} = f $$$$

Lean4

@[simp]
theorem flip_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : f.flip.flip = f :=
  by
  ext
  rfl

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