toPerfectPairingDual_apply — Mathlib

English

If N is in perfect pairing with M, then N is reflexive; equivalently, the reflexivity of M transfers to N via the duality e: N ≃ Dual M.

Русский

Если N находится в идеальной паре с M, тоN рефлексивен; рефлексивность переносится через дуальность e: N ≃ Dual M.

LaTeX

$$$N \text{ is reflexive }\\Rightarrow \\text{IsReflexive}(R,N).$$$

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
theorem toPerfectPairingDual_apply {f : Dual R M} {x : M} : IsReflexive.toPerfectPairingDual (R := R) f x = f x :=
  rfl

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