opContinuousLinearEquiv — Mathlib

English

The op function gives a continuous linear equivalence between M and its opposite.

Русский

Функция оп образует непрерывное линейное эквивалентное отображение между пространством и его противоположностью.

LaTeX

$$def opContinuousLinearEquiv : M ≃L[R] Mᵐᵒᵖ$$

Lean4

/-- The function `op` is a continuous linear equivalence. -/
@[simps!]
def opContinuousLinearEquiv : M ≃L[R] Mᵐᵒᵖ where __ := MulOpposite.opLinearEquiv R

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