instHasSolidNorm — Mathlib

English

The order dual αᵒᵈ of a normed lattice-ordered group α inherits a solid norm, i.e., HasSolidNorm (OrderDual α).

Русский

У порядка двойственной ориентации αᵒᵈ наследуется солидная норма; HasSolidNorm (OrderDual α).

LaTeX

$$$\text{HasSolidNorm}(α^{\mathrm{op}})$$$

Lean4

/-- Let `α` be a normed lattice ordered group, then the order dual is also a
normed lattice ordered group.
-/
instance (priority := 100) instHasSolidNorm : HasSolidNorm αᵒᵈ :=
  { solid := dual_solid (α := α) }

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