dual_dual_flip_dual — Mathlib

English

The double dual operation is idempotent in the sense that applying twice returns to the original dual.

Русский

Двойственное образование конуса повторно возвращает исходный двойной конус.

LaTeX

$$$\\operatorname{dual}(\\operatorname{dual}(p\\,\\mathrm{flip}(s))) = \\operatorname{dual}(p)(s)$$$

Lean4

@[simp]
theorem dual_dual_flip_dual : dual p (dual p.flip (dual p s)) = dual p s :=
  le_antisymm (dual_le_dual subset_dual_dual) subset_dual_dual

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