toDualProdHom — Mathlib

English

There is an order-embedding from NonemptyInterval α into the product αᵒᵈ × α, given by the map toDualProd.

Русский

Существует вложение порядка из NonemptyInterval α в произведение α с противоположным порядком и α, заданное отображением toDualProd.

LaTeX

$$$\text{toDualProdHom} : \text{NonemptyInterval } \alpha \hookrightarrow_o (\alpha^{\mathrm{op}} \times \alpha)$$$

Lean4

/-- `toDualProd` as an order embedding. -/
@[simps]
def toDualProdHom : NonemptyInterval α ↪o αᵒᵈ × α
    where
  toFun := toDualProd
  inj' := toDualProd_injective
  map_rel_iff' := Iff.rfl

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