orderEmbedding — Mathlib

English

There is an order-embedding of Submodule R p into Submodule R M.

Русский

Существование отображения-встраивания сложности порядка Submodule R p в Submodule R M.

LaTeX

$$$$ \mathrm{orderEmbedding} : \text{Submodule }R p \hookrightarrow \text{Submodule }R M $$$$

Lean4

/-- If `p ⊆ M` is a submodule, the ordering of submodules of `p` is embedded in the ordering of
submodules of `M`. -/
def orderEmbedding : Submodule R p ↪o Submodule R M :=
  (RelIso.toRelEmbedding <| MapSubtype.orderIso p).trans <|
    Subtype.relEmbedding (X := Submodule R M) (fun p p' ↦ p ≤ p') _

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