flip — Mathlib

English

The flip operation on a perfect pairing yields a new perfect pairing with the roles of M and N swapped, i.e. p.flip is a PerfectPairing R N M.

Русский

Переключение ролей через flip дает новую совершенную пару между N и M: p.flip — это PerfectPairing R N M.

LaTeX

$$$p.flip \text{ is a PerfectPairing } R N M$.$$

Lean4

protected theorem flip (h : p.IsPerfectCompl U V) : p.flip.IsPerfectCompl V U
    where
  isCompl_left := h.isCompl_right
  isCompl_right := h.isCompl_left

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