symm_dual_id — Mathlib

English

The dual of the inverse of the dual of the identity Inf/sup morphism equals the identity morphism: sSupHom.dual.symm (sInfHom.id _) = sSupHom.id α.

Русский

Дуальная обратная от дуального отображения для идентичности совпадает с идентичностью.

LaTeX

$$$sSupHom.dual.symm (sInfHom.id \\alpha) = sSupHom.id \\alpha$$$

Lean4

@[simp]
theorem symm_dual_id : sSupHom.dual.symm (sInfHom.id _) = sSupHom.id α :=
  rfl

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