instIsContPerfPair — Mathlib

English

Given a perfect pairing, flipping the roles of M and N yields an is_continuous_perfect_pair instance for the flipped bilinear map.

Русский

При совершенном парном отображении разворот ролей M и N дает экземпляр IsContPerfPair для пары в обратном порядке.

LaTeX

$$$p.flip.IsContPerfPair$$$

Lean4

/-- Given a perfect pairing between `M`and `N`, we may interchange the roles of `M` and `N`. -/
instance instIsContPerfPair : p.flip.IsContPerfPair
    where
  continuous_uncurry := p.continuous_uncurry_of_isContPerfPair.comp continuous_swap
  bijective_left := IsContPerfPair.bijective_right p
  bijective_right := IsContPerfPair.bijective_left p

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