comapMkQOrderEmbedding — Mathlib

English

The canonical equality of the order embedding equals the direct comap along the quotient map: comapMkQOrderEmbedding p p' = comap p.mkQ p'.

Русский

Эквивалентное равенство вложения в порядке: comapMkQOrderEmbedding p p' = comap p.mkQ p'.

LaTeX

$$$$ comapMkQOrderEmbedding\; p\; p' = comap p.mkQ p'. $$$$

Lean4

/-- The ordering on submodules of the quotient of `M` by `p` embeds into the ordering on submodules
of `M`. -/
def comapMkQOrderEmbedding : Submodule R (M ⧸ p) ↪o Submodule R M :=
  (RelIso.toRelEmbedding <| comapMkQRelIso p).trans (Subtype.relEmbedding (· ≤ ·) _)

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