toSubmodule' — Mathlib

English

The forgetful map from NonUnitalSubalgebra to Submodule is an order-embedding.

Русский

Отображение от NonUnitalSubalgebra к Submodule является вложением по порядку.

LaTeX

$$def toSubmodule' : NonUnitalSubalgebra(R,A) ↪o Submodule(R,A)$$

Lean4

/-- The forgetful map from `NonUnitalSubalgebra` to `Submodule` as an `OrderEmbedding` -/
def toSubmodule' [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonUnitalSubalgebra R A ↪o Submodule R A
    where
  toEmbedding :=
    { toFun := fun S => S.toSubmodule
      inj' := fun S T h => ext <| by apply SetLike.ext_iff.1 h }
  map_rel_iff' := SetLike.coe_subset_coe.symm.trans SetLike.coe_subset_coe

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