dual — Mathlib

English

An order embedding is also an order embedding between dual orders.

Русский

Вложение порядка также является вложением между двойственными порядками.

LaTeX

$$$\\text{dual}: (\\alpha \\hookrightarrow_o \\beta) \\to (\\alpha^{\\mathrm{op}} \\hookrightarrow_o \\beta^{\\mathrm{op}}).$$$

Lean4

/-- An order embedding is also an order embedding between dual orders. -/
protected def dual : αᵒᵈ ↪o βᵒᵈ :=
  ⟨f.toEmbedding, f.map_rel_iff⟩

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