ulift — Mathlib

English

The inverse of the inverse construction is obtained by swapping arguments; i.e., symmetry of equivOfInverse'

Русский

Обратное к конструктору обратного отображения достигается перестановкой аргументов; симметрия equivOfInverse'.

LaTeX

$$$(equivOfInverse f_1 f_2 h_1 h_2)^{-1} = equivOfInverse(f_2 f_1 h_2 h_1)$$$

Lean4

/-- The continuous linear equivalence between `ULift M₁` and `M₁`.

This is a continuous version of `ULift.moduleEquiv`. -/
def ulift : ULift M₁ ≃L[R₁] M₁ :=
  { ULift.moduleEquiv with
    continuous_toFun := continuous_uliftDown
    continuous_invFun := continuous_uliftUp }

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