of_bijective — Mathlib

English

If p : M →ₗ[R] N →ₗ[R] R is bijective and N is reflexive, then p is a perfect pairing.

Русский

Если линеарное отображение p : M →ₗ[R] N →ₗ[R] R биективно и N рефлексивно, то p является совершенной парой.

LaTeX

$$$\text{IsReflexive}(R,N) \;\Rightarrow\; \text{Bijective}(p) \Rightarrow \text{IsPerfPair}(p)$$$

Lean4

theorem of_bijective (p : M →ₗ[R] N →ₗ[R] R) [IsReflexive R N] (h : Bijective p) : IsPerfPair p :=
  inferInstanceAs
    ((LinearMap.id (R := R) (M := Dual R N)).compl₁₂ (LinearEquiv.ofBijective p h : M →ₗ[R] N →ₗ[R] R)
        (LinearEquiv.refl R N : N →ₗ[R] N)).IsPerfPair

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